ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>PseudoMetricSpace α<VAR>PseudoMetricSpace β<VAR>K : ℝ≥0<VAR>f : α → β<VAR>hf : AntilipschitzWith K f<GOAL>Filter.Tendsto f (Bornology.cobounded α) (Bornology.cobounded β)
<VAR>β : Type u_2<VAR>PseudoMetricSpace β<VAR>α : Type u_4<VAR>MetricSpace α<VAR>K : ℝ≥0<VAR>f : α → β<VAR>ProperSpace α<VAR>hK : AntilipschitzWith K f<VAR>f_cont : Continuous f<VAR>hf : Function.Surjective f<GOAL>ProperSpace β
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>PseudoMetricSpace α<VAR>PseudoMetricSpace β<VAR>PseudoMetricSpace γ<VAR>f : α → β → γ<VAR>K₁ : ℝ≥0<VAR>hf : ∀ (b : β), AntilipschitzWith K₁ fun a => f a b<VAR>s : Set α<VAR>t : Set β<VAR>hst : Bornology.IsBounded (Set.image2 f s t)<GOAL>Bornology.IsBounded s ∨ Bornology.IsBounded t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>PseudoMetricSpace α<VAR>PseudoMetricSpace β<VAR>PseudoMetricSpace γ<VAR>f : α → β → γ<VAR>K₂ : ℝ≥0<VAR>hf : ∀ (a : α), AntilipschitzWith K₂ (f a)<VAR>s : Set α<VAR>t : Set β<VAR>hst : Bornology.IsBounded (Set.image2 f s t)<GOAL>Bornology.IsBounded s ∨ Bornology.IsBounded t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>K : ℝ≥0<VAR>f : α → β<VAR>hf : LipschitzWith K f<VAR>g : β → α<VAR>hg : Function.RightInverse g f<GOAL>AntilipschitzWith K g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>PseudoMetricSpace α<VAR>MetricSpace β<VAR>ProperSpace β<VAR>K : ℝ≥0<VAR>f : α ≃ₜ β<VAR>hK : LipschitzWith K ⇑f<GOAL>ProperSpace α
<VAR>R : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>Semiring R<VAR>TopologicalSpace F<VAR>TopologicalSpace B<VAR>AddCommMonoid F<VAR>Module R F<VAR>(x : B) → AddCommMonoid (E x)<VAR>(x : B) → Module R (E x)<VAR>e : Pretrivialization F Bundle.TotalSpace.proj<VAR>self : Pretrivialization.IsLinear R e<VAR>b : B<GOAL>b ∈ e.baseSet → IsLinearMap R fun x => (↑e { proj := b, snd := x }).2
<VAR>R : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>Semiring R<VAR>TopologicalSpace F<VAR>TopologicalSpace B<VAR>e : Pretrivialization F Bundle.TotalSpace.proj<VAR>AddCommMonoid F<VAR>Module R F<VAR>(x : B) → AddCommMonoid (E x)<VAR>(x : B) → Module R (E x)<VAR>Pretrivialization.IsLinear R e<VAR>b : B<VAR>hb : b ∈ e.baseSet<GOAL>IsLinearMap R fun x => (↑e { proj := b, snd := x }).2
<VAR>R : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>Semiring R<VAR>TopologicalSpace F<VAR>TopologicalSpace B<VAR>AddCommMonoid F<VAR>Module R F<VAR>(x : B) → AddCommMonoid (E x)<VAR>(x : B) → Module R (E x)<VAR>e : Pretrivialization F Bundle.TotalSpace.proj<VAR>Pretrivialization.IsLinear R e<VAR>b : B<VAR>y : F<GOAL>(Pretrivialization.symmₗ R e b) y = e.symm b y
<VAR>R : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>Semiring R<VAR>TopologicalSpace F<VAR>TopologicalSpace B<VAR>AddCommMonoid F<VAR>Module R F<VAR>(x : B) → AddCommMonoid (E x)<VAR>(x : B) → Module R (E x)<VAR>e : Pretrivialization F Bundle.TotalSpace.proj<VAR>Pretrivialization.IsLinear R e<VAR>b : B<VAR>hb : b ∈ e.baseSet<GOAL>⇑(Pretrivialization.linearEquivAt R e b hb) = fun y => (↑e { proj := b, snd := y }).2
<VAR>R : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>Semiring R<VAR>TopologicalSpace F<VAR>TopologicalSpace B<VAR>AddCommMonoid F<VAR>Module R F<VAR>(x : B) → AddCommMonoid (E x)<VAR>(x : B) → Module R (E x)<VAR>e : Pretrivialization F Bundle.TotalSpace.proj<VAR>Pretrivialization.IsLinear R e<VAR>b : B<VAR>hb : b ∈ e.baseSet<GOAL>⇑(Pretrivialization.linearEquivAt R e b hb).symm = e.symm b
<VAR>R : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>Semiring R<VAR>TopologicalSpace F<VAR>TopologicalSpace B<VAR>AddCommMonoid F<VAR>Module R F<VAR>(x : B) → AddCommMonoid (E x)<VAR>(x : B) → Module R (E x)<VAR>e : Pretrivialization F Bundle.TotalSpace.proj<VAR>Pretrivialization.IsLinear R e<VAR>b : B<GOAL>⇑(Pretrivialization.linearMapAt R e b) = fun y => if b ∈ e.baseSet then (↑e { proj := b, snd := y }).2 else 0
<VAR>R : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>Semiring R<VAR>TopologicalSpace F<VAR>TopologicalSpace B<VAR>AddCommMonoid F<VAR>Module R F<VAR>(x : B) → AddCommMonoid (E x)<VAR>(x : B) → Module R (E x)<VAR>e : Pretrivialization F Bundle.TotalSpace.proj<VAR>Pretrivialization.IsLinear R e<VAR>b : B<VAR>hb : b ∈ e.baseSet<GOAL>⇑(Pretrivialization.linearMapAt R e b) = fun y => (↑e { proj := b, snd := y }).2
<VAR>R : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>Semiring R<VAR>TopologicalSpace F<VAR>TopologicalSpace B<VAR>AddCommMonoid F<VAR>Module R F<VAR>(x : B) → AddCommMonoid (E x)<VAR>(x : B) → Module R (E x)<VAR>e : Pretrivialization F Bundle.TotalSpace.proj<VAR>Pretrivialization.IsLinear R e<VAR>b : B<VAR>y : E b<GOAL>(Pretrivialization.linearMapAt R e b) y = if b ∈ e.baseSet then (↑e { proj := b, snd := y }).2 else 0
<VAR>R : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>Semiring R<VAR>TopologicalSpace F<VAR>TopologicalSpace B<VAR>AddCommMonoid F<VAR>Module R F<VAR>(x : B) → AddCommMonoid (E x)<VAR>(x : B) → Module R (E x)<VAR>e : Pretrivialization F Bundle.TotalSpace.proj<VAR>Pretrivialization.IsLinear R e<VAR>b : B<VAR>hb : b ∈ e.baseSet<GOAL>Pretrivialization.linearMapAt R e b = ↑(Pretrivialization.linearEquivAt R e b hb)
<VAR>R : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>Semiring R<VAR>TopologicalSpace F<VAR>TopologicalSpace B<VAR>AddCommMonoid F<VAR>Module R F<VAR>(x : B) → AddCommMonoid (E x)<VAR>(x : B) → Module R (E x)<VAR>e : Pretrivialization F Bundle.TotalSpace.proj<VAR>Pretrivialization.IsLinear R e<VAR>b : B<VAR>hb : b ∉ e.baseSet<GOAL>Pretrivialization.linearMapAt R e b = 0
<VAR>R : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>Semiring R<VAR>TopologicalSpace F<VAR>TopologicalSpace B<VAR>AddCommMonoid F<VAR>Module R F<VAR>(x : B) → AddCommMonoid (E x)<VAR>(x : B) → Module R (E x)<VAR>e : Pretrivialization F Bundle.TotalSpace.proj<VAR>Pretrivialization.IsLinear R e<VAR>b : B<VAR>hb : b ∈ e.baseSet<VAR>y : E b<GOAL>(Pretrivialization.symmₗ R e b) ((Pretrivialization.linearMapAt R e b) y) = y
<VAR>R : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>Semiring R<VAR>TopologicalSpace F<VAR>TopologicalSpace B<VAR>AddCommMonoid F<VAR>Module R F<VAR>(x : B) → AddCommMonoid (E x)<VAR>(x : B) → Module R (E x)<VAR>e : Pretrivialization F Bundle.TotalSpace.proj<VAR>Pretrivialization.IsLinear R e<VAR>b : B<VAR>hb : b ∈ e.baseSet<VAR>y : F<GOAL>(Pretrivialization.linearMapAt R e b) ((Pretrivialization.symmₗ R e b) y) = y
<VAR>R : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>Semiring R<VAR>TopologicalSpace F<VAR>TopologicalSpace B<VAR>TopologicalSpace (Bundle.TotalSpace F E)<VAR>AddCommMonoid F<VAR>Module R F<VAR>(x : B) → AddCommMonoid (E x)<VAR>(x : B) → Module R (E x)<VAR>e : Trivialization F Bundle.TotalSpace.proj<VAR>self : Trivialization.IsLinear R e<VAR>b : B<GOAL>b ∈ e.baseSet → IsLinearMap R fun x => (↑e { proj := b, snd := x }).2
<VAR>R : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>Semiring R<VAR>TopologicalSpace F<VAR>TopologicalSpace B<VAR>TopologicalSpace (Bundle.TotalSpace F E)<VAR>e : Trivialization F Bundle.TotalSpace.proj<VAR>AddCommMonoid F<VAR>Module R F<VAR>(x : B) → AddCommMonoid (E x)<VAR>(x : B) → Module R (E x)<VAR>Trivialization.IsLinear R e<VAR>b : B<VAR>hb : b ∈ e.baseSet<GOAL>IsLinearMap R fun y => (↑e { proj := b, snd := y }).2
<VAR>R : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>Semiring R<VAR>TopologicalSpace F<VAR>TopologicalSpace B<VAR>TopologicalSpace (Bundle.TotalSpace F E)<VAR>AddCommMonoid F<VAR>Module R F<VAR>(x : B) → AddCommMonoid (E x)<VAR>(x : B) → Module R (E x)<VAR>e : Trivialization F Bundle.TotalSpace.proj<VAR>Trivialization.IsLinear R e<VAR>b : B<VAR>hb : b ∈ e.baseSet<VAR>v : E b<GOAL>(Trivialization.linearEquivAt R e b hb) v = (↑e { proj := b, snd := v }).2
<VAR>R : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>Semiring R<VAR>TopologicalSpace F<VAR>TopologicalSpace B<VAR>TopologicalSpace (Bundle.TotalSpace F E)<VAR>AddCommMonoid F<VAR>Module R F<VAR>(x : B) → AddCommMonoid (E x)<VAR>(x : B) → Module R (E x)<VAR>e : Trivialization F Bundle.TotalSpace.proj<VAR>Trivialization.IsLinear R e<VAR>b : B<VAR>hb : b ∈ e.baseSet<VAR>v : F<GOAL>(Trivialization.linearEquivAt R e b hb).symm v = e.symm b v
<VAR>R : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>Semiring R<VAR>TopologicalSpace F<VAR>TopologicalSpace B<VAR>TopologicalSpace (Bundle.TotalSpace F E)<VAR>AddCommMonoid F<VAR>Module R F<VAR>(x : B) → AddCommMonoid (E x)<VAR>(x : B) → Module R (E x)<VAR>e : Trivialization F Bundle.TotalSpace.proj<VAR>Trivialization.IsLinear R e<VAR>b : B<GOAL>⇑(Trivialization.symmₗ R e b) = e.symm b
<VAR>R : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>Semiring R<VAR>TopologicalSpace F<VAR>TopologicalSpace B<VAR>TopologicalSpace (Bundle.TotalSpace F E)<VAR>AddCommMonoid F<VAR>Module R F<VAR>(x : B) → AddCommMonoid (E x)<VAR>(x : B) → Module R (E x)<VAR>e : Trivialization F Bundle.TotalSpace.proj<VAR>Trivialization.IsLinear R e<VAR>b : B<GOAL>⇑(Trivialization.linearMapAt R e b) = fun y => if b ∈ e.baseSet then (↑e { proj := b, snd := y }).2 else 0
<VAR>R : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>Semiring R<VAR>TopologicalSpace F<VAR>TopologicalSpace B<VAR>TopologicalSpace (Bundle.TotalSpace F E)<VAR>AddCommMonoid F<VAR>Module R F<VAR>(x : B) → AddCommMonoid (E x)<VAR>(x : B) → Module R (E x)<VAR>e : Trivialization F Bundle.TotalSpace.proj<VAR>Trivialization.IsLinear R e<VAR>b : B<VAR>hb : b ∈ e.baseSet<GOAL>⇑(Trivialization.linearMapAt R e b) = fun y => (↑e { proj := b, snd := y }).2
<VAR>R : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>Semiring R<VAR>TopologicalSpace F<VAR>TopologicalSpace B<VAR>TopologicalSpace (Bundle.TotalSpace F E)<VAR>AddCommMonoid F<VAR>Module R F<VAR>(x : B) → AddCommMonoid (E x)<VAR>(x : B) → Module R (E x)<VAR>e : Trivialization F Bundle.TotalSpace.proj<VAR>Trivialization.IsLinear R e<VAR>b : B<VAR>y : E b<GOAL>(Trivialization.linearMapAt R e b) y = if b ∈ e.baseSet then (↑e { proj := b, snd := y }).2 else 0
<VAR>R : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>Semiring R<VAR>TopologicalSpace F<VAR>TopologicalSpace B<VAR>TopologicalSpace (Bundle.TotalSpace F E)<VAR>AddCommMonoid F<VAR>Module R F<VAR>(x : B) → AddCommMonoid (E x)<VAR>(x : B) → Module R (E x)<VAR>e : Trivialization F Bundle.TotalSpace.proj<VAR>Trivialization.IsLinear R e<VAR>b : B<VAR>hb : b ∈ e.baseSet<GOAL>Trivialization.linearMapAt R e b = ↑(Trivialization.linearEquivAt R e b hb)
<VAR>R : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>Semiring R<VAR>TopologicalSpace F<VAR>TopologicalSpace B<VAR>TopologicalSpace (Bundle.TotalSpace F E)<VAR>AddCommMonoid F<VAR>Module R F<VAR>(x : B) → AddCommMonoid (E x)<VAR>(x : B) → Module R (E x)<VAR>e : Trivialization F Bundle.TotalSpace.proj<VAR>Trivialization.IsLinear R e<VAR>b : B<VAR>hb : b ∉ e.baseSet<GOAL>Trivialization.linearMapAt R e b = 0
<VAR>R : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>Semiring R<VAR>TopologicalSpace F<VAR>TopologicalSpace B<VAR>TopologicalSpace (Bundle.TotalSpace F E)<VAR>AddCommMonoid F<VAR>Module R F<VAR>(x : B) → AddCommMonoid (E x)<VAR>(x : B) → Module R (E x)<VAR>e : Trivialization F Bundle.TotalSpace.proj<VAR>Trivialization.IsLinear R e<VAR>b : B<VAR>hb : b ∈ e.baseSet<VAR>y : E b<GOAL>(Trivialization.symmₗ R e b) ((Trivialization.linearMapAt R e b) y) = y
<VAR>R : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>Semiring R<VAR>TopologicalSpace F<VAR>TopologicalSpace B<VAR>TopologicalSpace (Bundle.TotalSpace F E)<VAR>AddCommMonoid F<VAR>Module R F<VAR>(x : B) → AddCommMonoid (E x)<VAR>(x : B) → Module R (E x)<VAR>e : Trivialization F Bundle.TotalSpace.proj<VAR>Trivialization.IsLinear R e<VAR>b : B<VAR>hb : b ∈ e.baseSet<VAR>y : F<GOAL>(Trivialization.linearMapAt R e b) ((Trivialization.symmₗ R e b) y) = y
<VAR>R : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>Semiring R<VAR>TopologicalSpace F<VAR>TopologicalSpace B<VAR>TopologicalSpace (Bundle.TotalSpace F E)<VAR>AddCommMonoid F<VAR>Module R F<VAR>(x : B) → AddCommMonoid (E x)<VAR>(x : B) → Module R (E x)<VAR>e e' : Trivialization F Bundle.TotalSpace.proj<VAR>Trivialization.IsLinear R e<VAR>Trivialization.IsLinear R e'<VAR>b : B<VAR>hb : b ∈ e.baseSet ∩ e'.baseSet<GOAL>⇑(Trivialization.coordChangeL R e e' b) = ⇑((Trivialization.linearEquivAt R e b ⋯).symm ≪≫ₗ Trivialization.linearEquivAt R e' b ⋯)
<VAR>R : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>Semiring R<VAR>TopologicalSpace F<VAR>TopologicalSpace B<VAR>TopologicalSpace (Bundle.TotalSpace F E)<VAR>AddCommMonoid F<VAR>Module R F<VAR>(x : B) → AddCommMonoid (E x)<VAR>(x : B) → Module R (E x)<VAR>e e' : Trivialization F Bundle.TotalSpace.proj<VAR>Trivialization.IsLinear R e<VAR>Trivialization.IsLinear R e'<VAR>b : B<VAR>hb : b ∈ e.baseSet ∩ e'.baseSet<GOAL>(Trivialization.coordChangeL R e e' b).toLinearEquiv = (Trivialization.linearEquivAt R e b ⋯).symm ≪≫ₗ Trivialization.linearEquivAt R e' b ⋯
<VAR>R : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>Semiring R<VAR>TopologicalSpace F<VAR>TopologicalSpace B<VAR>TopologicalSpace (Bundle.TotalSpace F E)<VAR>AddCommMonoid F<VAR>Module R F<VAR>(x : B) → AddCommMonoid (E x)<VAR>(x : B) → Module R (E x)<VAR>e e' : Trivialization F Bundle.TotalSpace.proj<VAR>Trivialization.IsLinear R e<VAR>Trivialization.IsLinear R e'<VAR>b : B<VAR>hb : b ∈ e'.baseSet ∩ e.baseSet<GOAL>(Trivialization.coordChangeL R e e' b).symm = Trivialization.coordChangeL R e' e b
<VAR>R : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>Semiring R<VAR>TopologicalSpace F<VAR>TopologicalSpace B<VAR>TopologicalSpace (Bundle.TotalSpace F E)<VAR>AddCommMonoid F<VAR>Module R F<VAR>(x : B) → AddCommMonoid (E x)<VAR>(x : B) → Module R (E x)<VAR>e e' : Trivialization F Bundle.TotalSpace.proj<VAR>Trivialization.IsLinear R e<VAR>Trivialization.IsLinear R e'<VAR>b : B<VAR>hb : b ∈ e.baseSet ∩ e'.baseSet<VAR>y : F<GOAL>(Trivialization.coordChangeL R e e' b) y = (↑e' { proj := b, snd := e.symm b y }).2
<VAR>R : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>Semiring R<VAR>TopologicalSpace F<VAR>TopologicalSpace B<VAR>TopologicalSpace (Bundle.TotalSpace F E)<VAR>AddCommMonoid F<VAR>Module R F<VAR>(x : B) → AddCommMonoid (E x)<VAR>(x : B) → Module R (E x)<VAR>e e' : Trivialization F Bundle.TotalSpace.proj<VAR>Trivialization.IsLinear R e<VAR>Trivialization.IsLinear R e'<VAR>b : B<VAR>hb : b ∈ e.baseSet ∩ e'.baseSet<VAR>y : F<GOAL>(b, (Trivialization.coordChangeL R e e' b) y) = ↑e' { proj := b, snd := e.symm b y }
<VAR>R : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>Semiring R<VAR>TopologicalSpace F<VAR>TopologicalSpace B<VAR>TopologicalSpace (Bundle.TotalSpace F E)<VAR>AddCommMonoid F<VAR>Module R F<VAR>(x : B) → AddCommMonoid (E x)<VAR>(x : B) → Module R (E x)<VAR>e e' : Trivialization F Bundle.TotalSpace.proj<VAR>Trivialization.IsLinear R e<VAR>Trivialization.IsLinear R e'<VAR>b : B<VAR>hb : b ∈ e.baseSet ∩ e'.baseSet<VAR>v : F<GOAL>↑e' (↑e.symm (b, v)) = (b, (Trivialization.coordChangeL R e e' b) v)
<VAR>R : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>Semiring R<VAR>TopologicalSpace F<VAR>TopologicalSpace B<VAR>TopologicalSpace (Bundle.TotalSpace F E)<VAR>AddCommMonoid F<VAR>Module R F<VAR>(x : B) → AddCommMonoid (E x)<VAR>(x : B) → Module R (E x)<VAR>e e' : Trivialization F Bundle.TotalSpace.proj<VAR>Trivialization.IsLinear R e<VAR>Trivialization.IsLinear R e'<VAR>b : B<VAR>hb : b ∈ e.baseSet ∩ e'.baseSet<VAR>y : F<GOAL>(Trivialization.coordChangeL R e e' b) y = (↑e' (↑e.symm (b, y))).2
<VAR>R : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>Semiring R<VAR>TopologicalSpace F<VAR>TopologicalSpace B<VAR>TopologicalSpace (Bundle.TotalSpace F E)<VAR>AddCommMonoid F<VAR>Module R F<VAR>(x : B) → AddCommMonoid (E x)<VAR>(x : B) → Module R (E x)<VAR>e e' : Trivialization F Bundle.TotalSpace.proj<VAR>Trivialization.IsLinear R e<VAR>Trivialization.IsLinear R e'<VAR>b : B<VAR>hb : b ∈ e.baseSet ∩ e'.baseSet<GOAL>⇑(Trivialization.coordChangeL R e e' b).symm = ⇑((Trivialization.linearEquivAt R e' b ⋯).symm ≪≫ₗ Trivialization.linearEquivAt R e b ⋯)
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>(x : B) → Zero (E x)<VAR>x : B<GOAL>(Bundle.zeroSection F E x).proj = x
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>(x : B) → Zero (E x)<VAR>x : B<GOAL>(Bundle.zeroSection F E x).snd = 0
<VAR>R : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>NontriviallyNormedField R<VAR>(x : B) → AddCommMonoid (E x)<VAR>(x : B) → Module R (E x)<VAR>NormedAddCommGroup F<VAR>NormedSpace R F<VAR>TopologicalSpace B<VAR>TopologicalSpace (Bundle.TotalSpace F E)<VAR>(x : B) → TopologicalSpace (E x)<VAR>FiberBundle F E<VAR>self : VectorBundle R F E<VAR>e : Trivialization F Bundle.TotalSpace.proj<VAR>MemTrivializationAtlas e<GOAL>Trivialization.IsLinear R e
<VAR>R : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>NontriviallyNormedField R<VAR>(x : B) → AddCommMonoid (E x)<VAR>(x : B) → Module R (E x)<VAR>NormedAddCommGroup F<VAR>NormedSpace R F<VAR>TopologicalSpace B<VAR>TopologicalSpace (Bundle.TotalSpace F E)<VAR>(x : B) → TopologicalSpace (E x)<VAR>FiberBundle F E<VAR>self : VectorBundle R F E<VAR>e e' : Trivialization F Bundle.TotalSpace.proj<VAR>MemTrivializationAtlas e<VAR>MemTrivializationAtlas e'<GOAL>ContinuousOn (fun b => ↑(Trivialization.coordChangeL R e e' b)) (e.baseSet ∩ e'.baseSet)
<VAR>R : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>NontriviallyNormedField R<VAR>(x : B) → AddCommMonoid (E x)<VAR>(x : B) → Module R (E x)<VAR>NormedAddCommGroup F<VAR>NormedSpace R F<VAR>TopologicalSpace B<VAR>TopologicalSpace (Bundle.TotalSpace F E)<VAR>(x : B) → TopologicalSpace (E x)<VAR>FiberBundle F E<VAR>VectorBundle R F E<VAR>e e' : Trivialization F Bundle.TotalSpace.proj<VAR>MemTrivializationAtlas e<VAR>MemTrivializationAtlas e'<GOAL>ContinuousOn (fun b => ↑(Trivialization.coordChangeL R e e' b)) (e.baseSet ∩ e'.baseSet)
<VAR>R : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>NontriviallyNormedField R<VAR>(x : B) → AddCommMonoid (E x)<VAR>(x : B) → Module R (E x)<VAR>NormedAddCommGroup F<VAR>NormedSpace R F<VAR>TopologicalSpace B<VAR>TopologicalSpace (Bundle.TotalSpace F E)<VAR>(x : B) → TopologicalSpace (E x)<VAR>FiberBundle F E<VAR>e : Trivialization F Bundle.TotalSpace.proj<VAR>Trivialization.IsLinear R e<VAR>b : B<GOAL>⇑(Trivialization.continuousLinearMapAt R e b) = ⇑(Trivialization.linearMapAt R e b)
<VAR>R : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>NontriviallyNormedField R<VAR>(x : B) → AddCommMonoid (E x)<VAR>(x : B) → Module R (E x)<VAR>NormedAddCommGroup F<VAR>NormedSpace R F<VAR>TopologicalSpace B<VAR>TopologicalSpace (Bundle.TotalSpace F E)<VAR>(x : B) → TopologicalSpace (E x)<VAR>FiberBundle F E<VAR>e : Trivialization F Bundle.TotalSpace.proj<VAR>Trivialization.IsLinear R e<VAR>b : B<GOAL>⇑(Trivialization.symmL R e b) = e.symm b
<VAR>R : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>NontriviallyNormedField R<VAR>(x : B) → AddCommMonoid (E x)<VAR>(x : B) → Module R (E x)<VAR>NormedAddCommGroup F<VAR>NormedSpace R F<VAR>TopologicalSpace B<VAR>TopologicalSpace (Bundle.TotalSpace F E)<VAR>(x : B) → TopologicalSpace (E x)<VAR>FiberBundle F E<VAR>e : Trivialization F Bundle.TotalSpace.proj<VAR>Trivialization.IsLinear R e<VAR>b : B<VAR>hb : b ∈ e.baseSet<VAR>y : E b<GOAL>(Trivialization.symmL R e b) ((Trivialization.continuousLinearMapAt R e b) y) = y
<VAR>R : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>NontriviallyNormedField R<VAR>(x : B) → AddCommMonoid (E x)<VAR>(x : B) → Module R (E x)<VAR>NormedAddCommGroup F<VAR>NormedSpace R F<VAR>TopologicalSpace B<VAR>TopologicalSpace (Bundle.TotalSpace F E)<VAR>(x : B) → TopologicalSpace (E x)<VAR>FiberBundle F E<VAR>e : Trivialization F Bundle.TotalSpace.proj<VAR>Trivialization.IsLinear R e<VAR>b : B<VAR>hb : b ∈ e.baseSet<VAR>y : F<GOAL>(Trivialization.continuousLinearMapAt R e b) ((Trivialization.symmL R e b) y) = y
<VAR>R : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>NontriviallyNormedField R<VAR>(x : B) → AddCommMonoid (E x)<VAR>(x : B) → Module R (E x)<VAR>NormedAddCommGroup F<VAR>NormedSpace R F<VAR>TopologicalSpace B<VAR>TopologicalSpace (Bundle.TotalSpace F E)<VAR>(x : B) → TopologicalSpace (E x)<VAR>FiberBundle F E<VAR>e : Trivialization F Bundle.TotalSpace.proj<VAR>Trivialization.IsLinear R e<VAR>b : B<VAR>hb : b ∈ e.baseSet<GOAL>⇑(Trivialization.continuousLinearEquivAt R e b hb) = fun y => (↑e { proj := b, snd := y }).2
<VAR>R : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>NontriviallyNormedField R<VAR>(x : B) → AddCommMonoid (E x)<VAR>(x : B) → Module R (E x)<VAR>NormedAddCommGroup F<VAR>NormedSpace R F<VAR>TopologicalSpace B<VAR>TopologicalSpace (Bundle.TotalSpace F E)<VAR>(x : B) → TopologicalSpace (E x)<VAR>FiberBundle F E<VAR>e : Trivialization F Bundle.TotalSpace.proj<VAR>Trivialization.IsLinear R e<VAR>b : B<VAR>hb : b ∈ e.baseSet<GOAL>⇑(Trivialization.continuousLinearEquivAt R e b hb).symm = e.symm b
<VAR>R : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>NontriviallyNormedField R<VAR>(x : B) → AddCommMonoid (E x)<VAR>(x : B) → Module R (E x)<VAR>NormedAddCommGroup F<VAR>NormedSpace R F<VAR>TopologicalSpace B<VAR>TopologicalSpace (Bundle.TotalSpace F E)<VAR>(x : B) → TopologicalSpace (E x)<VAR>FiberBundle F E<VAR>e : Trivialization F Bundle.TotalSpace.proj<VAR>Trivialization.IsLinear R e<VAR>b : B<VAR>hb : b ∈ e.baseSet<GOAL>⇑(Trivialization.continuousLinearEquivAt R e b hb) = ⇑(Trivialization.continuousLinearMapAt R e b)
<VAR>R : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>NontriviallyNormedField R<VAR>(x : B) → AddCommMonoid (E x)<VAR>(x : B) → Module R (E x)<VAR>NormedAddCommGroup F<VAR>NormedSpace R F<VAR>TopologicalSpace B<VAR>TopologicalSpace (Bundle.TotalSpace F E)<VAR>(x : B) → TopologicalSpace (E x)<VAR>FiberBundle F E<VAR>e : Trivialization F Bundle.TotalSpace.proj<VAR>Trivialization.IsLinear R e<VAR>b : B<VAR>hb : b ∈ e.baseSet<GOAL>⇑(Trivialization.continuousLinearEquivAt R e b hb).symm = ⇑(Trivialization.symmL R e b)
<VAR>R : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>NontriviallyNormedField R<VAR>(x : B) → AddCommMonoid (E x)<VAR>(x : B) → Module R (E x)<VAR>NormedAddCommGroup F<VAR>NormedSpace R F<VAR>TopologicalSpace B<VAR>TopologicalSpace (Bundle.TotalSpace F E)<VAR>(x : B) → TopologicalSpace (E x)<VAR>FiberBundle F E<VAR>e : Trivialization F Bundle.TotalSpace.proj<VAR>Trivialization.IsLinear R e<VAR>x : Bundle.TotalSpace F E<VAR>hx : x ∈ e.source<GOAL>(Trivialization.continuousLinearEquivAt R e x.proj ⋯) x.snd = (↑e x).2
<VAR>R : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>NontriviallyNormedField R<VAR>(x : B) → AddCommMonoid (E x)<VAR>(x : B) → Module R (E x)<VAR>NormedAddCommGroup F<VAR>NormedSpace R F<VAR>TopologicalSpace B<VAR>TopologicalSpace (Bundle.TotalSpace F E)<VAR>(x : B) → TopologicalSpace (E x)<VAR>FiberBundle F E<VAR>e : Trivialization F Bundle.TotalSpace.proj<VAR>Trivialization.IsLinear R e<VAR>b : B<VAR>hb : b ∈ e.baseSet<VAR>z : E b<GOAL>↑e { proj := b, snd := z } = (b, (Trivialization.continuousLinearEquivAt R e b hb) z)
<VAR>R : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>NontriviallyNormedField R<VAR>(x : B) → AddCommMonoid (E x)<VAR>(x : B) → Module R (E x)<VAR>NormedAddCommGroup F<VAR>NormedSpace R F<VAR>TopologicalSpace B<VAR>TopologicalSpace (Bundle.TotalSpace F E)<VAR>(x : B) → TopologicalSpace (E x)<VAR>FiberBundle F E<VAR>e : Trivialization F Bundle.TotalSpace.proj<VAR>Trivialization.IsLinear R e<VAR>x : B<VAR>hx : x ∈ e.baseSet<GOAL>↑e (Bundle.zeroSection F E x) = (x, 0)