ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>UniformSpace α<GOAL>UniformContinuous ↑α
<VAR>α : Type u_1<VAR>UniformSpace α<GOAL>Continuous ↑α
<VAR>α : Type u_1<VAR>UniformSpace α<VAR>T0Space α<GOAL>UniformEmbedding ↑α
<VAR>α : Type u_1<VAR>UniformSpace α<VAR>T0Space α<GOAL>Function.Injective ↑α
<VAR>α : Type u_1<VAR>UniformSpace α<GOAL>DenseInducing ↑α
<VAR>α : Type u_1<VAR>UniformSpace α<VAR>T0Space α<GOAL>DenseEmbedding ↑α
<VAR>α : Type u_1<VAR>UniformSpace α<VAR>β : Type u_2<VAR>UniformSpace β<GOAL>DenseRange fun x => (↑α x.1, ↑β x.2)
<VAR>α : Type u_1<VAR>UniformSpace α<VAR>β : Type u_2<VAR>UniformSpace β<VAR>γ : Type u_3<VAR>UniformSpace γ<GOAL>DenseRange fun x => (↑α x.1, ↑β x.2.1, ↑γ x.2.2)
<VAR>α : Type u_1<VAR>UniformSpace α<VAR>p : UniformSpace.Completion α → Prop<VAR>a : UniformSpace.Completion α<VAR>hp : IsClosed {a | p a}<VAR>ih : ∀ (a : α), p (↑α a)<GOAL>p a
<VAR>α : Type u_1<VAR>UniformSpace α<VAR>β : Type u_2<VAR>UniformSpace β<VAR>p : UniformSpace.Completion α → UniformSpace.Completion β → Prop<VAR>a : UniformSpace.Completion α<VAR>b : UniformSpace.Completion β<VAR>hp : IsClosed {x | p x.1 x.2}<VAR>ih : ∀ (a : α) (b : β), p (↑α a) (↑β b)<GOAL>p a b
<VAR>α : Type u_1<VAR>UniformSpace α<VAR>β : Type u_2<VAR>UniformSpace β<VAR>γ : Type u_3<VAR>UniformSpace γ<VAR>p : UniformSpace.Completion α → UniformSpace.Completion β → UniformSpace.Completion γ → Prop<VAR>a : UniformSpace.Completion α<VAR>b : UniformSpace.Completion β<VAR>c : UniformSpace.Completion γ<VAR>hp : IsClosed {x | p x.1 x.2.1 x.2.2}<VAR>ih : ∀ (a : α) (b : β) (c : γ), p (↑α a) (↑β b) (↑γ c)<GOAL>p a b c
<VAR>α : Type u_1<VAR>UniformSpace α<VAR>Y : Type u_4<VAR>TopologicalSpace Y<VAR>T2Space Y<VAR>f g : UniformSpace.Completion α → Y<VAR>hf : Continuous f<VAR>hg : Continuous g<VAR>h : ∀ (a : α), f (↑α a) = g (↑α a)<GOAL>f = g
<VAR>α : Type u_1<VAR>UniformSpace α<VAR>Y : Type u_4<VAR>TopologicalSpace Y<VAR>T2Space Y<VAR>f g : UniformSpace.Completion α → Y<VAR>hf : Continuous f<VAR>hg : Continuous g<VAR>h : ∀ (a : α), f (↑α a) = g (↑α a)<VAR>a : UniformSpace.Completion α<GOAL>f a = g a
<VAR>α : Type u_1<VAR>UniformSpace α<VAR>β : Type u_2<VAR>UniformSpace β<VAR>f : α → β<VAR>CompleteSpace β<GOAL>UniformContinuous (UniformSpace.Completion.extension f)
<VAR>α : Type u_1<VAR>UniformSpace α<VAR>β : Type u_2<VAR>UniformSpace β<VAR>f : α → β<VAR>CompleteSpace β<GOAL>Continuous (UniformSpace.Completion.extension f)
<VAR>α : Type u_1<VAR>UniformSpace α<VAR>β : Type u_2<VAR>UniformSpace β<VAR>f : α → β<VAR>T0Space β<VAR>hf : UniformContinuous f<VAR>a : α<GOAL>UniformSpace.Completion.extension f (↑α a) = f a
<VAR>α : Type u_1<VAR>UniformSpace α<VAR>β : Type u_2<VAR>UniformSpace β<VAR>f : α → β<VAR>T0Space β<VAR>CompleteSpace β<VAR>hf : UniformContinuous f<VAR>g : UniformSpace.Completion α → β<VAR>hg : UniformContinuous g<VAR>h : ∀ (a : α), f a = g (↑α a)<GOAL>UniformSpace.Completion.extension f = g
<VAR>α : Type u_1<VAR>UniformSpace α<VAR>β : Type u_2<VAR>UniformSpace β<VAR>T0Space β<VAR>CompleteSpace β<VAR>f : UniformSpace.Completion α → β<VAR>hf : UniformContinuous f<GOAL>UniformSpace.Completion.extension (f ∘ ↑α) = f
<VAR>α : Type u_1<VAR>UniformSpace α<VAR>β : Type u_2<VAR>UniformSpace β<VAR>f : α → β<GOAL>UniformContinuous (UniformSpace.Completion.map f)
<VAR>α : Type u_1<VAR>UniformSpace α<VAR>β : Type u_2<VAR>UniformSpace β<VAR>f : α → β<GOAL>Continuous (UniformSpace.Completion.map f)
<VAR>α : Type u_1<VAR>UniformSpace α<VAR>β : Type u_2<VAR>UniformSpace β<VAR>f : α → β<VAR>hf : UniformContinuous f<VAR>a : α<GOAL>UniformSpace.Completion.map f (↑α a) = ↑β (f a)
<VAR>α : Type u_1<VAR>UniformSpace α<VAR>β : Type u_2<VAR>UniformSpace β<VAR>f : α → β<VAR>g : UniformSpace.Completion α → UniformSpace.Completion β<VAR>hg : UniformContinuous g<VAR>h : ∀ (a : α), ↑β (f a) = g (↑α a)<GOAL>UniformSpace.Completion.map f = g
<VAR>α : Type u_1<VAR>UniformSpace α<GOAL>UniformSpace.Completion.map id = id
<VAR>α : Type u_1<VAR>UniformSpace α<VAR>β : Type u_2<VAR>UniformSpace β<VAR>γ : Type u_3<VAR>UniformSpace γ<VAR>CompleteSpace γ<VAR>T0Space γ<VAR>f : β → γ<VAR>g : α → β<VAR>hf : UniformContinuous f<VAR>hg : UniformContinuous g<GOAL>UniformSpace.Completion.extension f ∘ UniformSpace.Completion.map g = UniformSpace.Completion.extension (f ∘ g)
<VAR>α : Type u_1<VAR>UniformSpace α<VAR>β : Type u_2<VAR>UniformSpace β<VAR>γ : Type u_3<VAR>UniformSpace γ<VAR>g : β → γ<VAR>f : α → β<VAR>hg : UniformContinuous g<VAR>hf : UniformContinuous f<GOAL>UniformSpace.Completion.map g ∘ UniformSpace.Completion.map f = UniformSpace.Completion.map (g ∘ f)
<VAR>α : Type u_1<VAR>UniformSpace α<GOAL>UniformContinuous ⇑(UniformSpace.Completion.completionSeparationQuotientEquiv α)
<VAR>α : Type u_1<VAR>UniformSpace α<GOAL>UniformContinuous ⇑(UniformSpace.Completion.completionSeparationQuotientEquiv α).symm
<VAR>α : Type u_1<VAR>UniformSpace α<VAR>β : Type u_2<VAR>UniformSpace β<VAR>γ : Type u_3<VAR>UniformSpace γ<VAR>f : α → β → γ<VAR>T0Space γ<VAR>hf : UniformContinuous₂ f<VAR>a : α<VAR>b : β<GOAL>UniformSpace.Completion.extension₂ f (↑α a) (↑β b) = f a b
<VAR>α : Type u_1<VAR>UniformSpace α<VAR>β : Type u_2<VAR>UniformSpace β<VAR>γ : Type u_3<VAR>UniformSpace γ<VAR>f : α → β → γ<VAR>CompleteSpace γ<GOAL>UniformContinuous₂ (UniformSpace.Completion.extension₂ f)
<VAR>α : Type u_1<VAR>UniformSpace α<VAR>β : Type u_2<VAR>UniformSpace β<VAR>γ : Type u_3<VAR>UniformSpace γ<VAR>f : α → β → γ<GOAL>UniformContinuous₂ (UniformSpace.Completion.map₂ f)
<VAR>α : Type u_1<VAR>UniformSpace α<VAR>β : Type u_2<VAR>UniformSpace β<VAR>γ : Type u_3<VAR>UniformSpace γ<VAR>δ : Type u_4<VAR>TopologicalSpace δ<VAR>f : α → β → γ<VAR>a : δ → UniformSpace.Completion α<VAR>b : δ → UniformSpace.Completion β<VAR>ha : Continuous a<VAR>hb : Continuous b<GOAL>Continuous fun d => UniformSpace.Completion.map₂ f (a d) (b d)
<VAR>α : Type u_1<VAR>UniformSpace α<VAR>β : Type u_2<VAR>UniformSpace β<VAR>γ : Type u_3<VAR>UniformSpace γ<VAR>a : α<VAR>b : β<VAR>f : α → β → γ<VAR>hf : UniformContinuous₂ f<GOAL>UniformSpace.Completion.map₂ f (↑α a) (↑β b) = ↑γ (f a b)
<VAR>α : Type u<VAR>ι : Type v<VAR>MetricSpace α<VAR>ProperSpace α<VAR>c : ι → α<VAR>s : Set α<VAR>r : ι → ℝ<VAR>hs : IsClosed s<VAR>uf : ∀ x ∈ s, {i | x ∈ Metric.ball (c i) (r i)}.Finite<VAR>us : s ⊆ ⋃ i, Metric.ball (c i) (r i)<GOAL>∃ r', s ⊆ ⋃ i, Metric.ball (c i) (r' i) ∧ ∀ (i : ι), r' i < r i
<VAR>α : Type u<VAR>ι : Type v<VAR>MetricSpace α<VAR>ProperSpace α<VAR>c : ι → α<VAR>r : ι → ℝ<VAR>uf : ∀ (x : α), {i | x ∈ Metric.ball (c i) (r i)}.Finite<VAR>uU : ⋃ i, Metric.ball (c i) (r i) = Set.univ<GOAL>∃ r', ⋃ i, Metric.ball (c i) (r' i) = Set.univ ∧ ∀ (i : ι), r' i < r i
<VAR>α : Type u<VAR>ι : Type v<VAR>MetricSpace α<VAR>ProperSpace α<VAR>c : ι → α<VAR>s : Set α<VAR>r : ι → ℝ<VAR>hr : ∀ (i : ι), 0 < r i<VAR>hs : IsClosed s<VAR>uf : ∀ x ∈ s, {i | x ∈ Metric.ball (c i) (r i)}.Finite<VAR>us : s ⊆ ⋃ i, Metric.ball (c i) (r i)<GOAL>∃ r', s ⊆ ⋃ i, Metric.ball (c i) (r' i) ∧ ∀ (i : ι), r' i ∈ Set.Ioo 0 (r i)
<VAR>α : Type u<VAR>ι : Type v<VAR>MetricSpace α<VAR>ProperSpace α<VAR>c : ι → α<VAR>r : ι → ℝ<VAR>hr : ∀ (i : ι), 0 < r i<VAR>uf : ∀ (x : α), {i | x ∈ Metric.ball (c i) (r i)}.Finite<VAR>uU : ⋃ i, Metric.ball (c i) (r i) = Set.univ<GOAL>∃ r', ⋃ i, Metric.ball (c i) (r' i) = Set.univ ∧ ∀ (i : ι), r' i ∈ Set.Ioo 0 (r i)
<VAR>α : Type u<VAR>MetricSpace α<VAR>ProperSpace α<VAR>s : Set α<VAR>hs : IsClosed s<VAR>R : α → ℝ<VAR>hR : ∀ x ∈ s, 0 < R x<GOAL>∃ ι c r r', (∀ (i : ι), c i ∈ s ∧ 0 < r i ∧ r i < r' i ∧ r' i < R (c i)) ∧ (LocallyFinite fun i => Metric.ball (c i) (r' i)) ∧ s ⊆ ⋃ i, Metric.ball (c i) (r i)
<VAR>α : Type u<VAR>MetricSpace α<VAR>ProperSpace α<VAR>R : α → ℝ<VAR>hR : ∀ (x : α), 0 < R x<GOAL>∃ ι c r r', (∀ (i : ι), 0 < r i ∧ r i < r' i ∧ r' i < R (c i)) ∧ (LocallyFinite fun i => Metric.ball (c i) (r' i)) ∧ ⋃ i, Metric.ball (c i) (r i) = Set.univ
<VAR>ι : Type u_3<VAR>L : Filter ι<VAR>β : Type u_4<VAR>p : ι → Prop<VAR>DecidablePred p<VAR>q : Prop<VAR>Decidable q<VAR>a b : β<VAR>F G : Filter β<VAR>haG : {a}ᶜ ∈ G<VAR>hbF : {b}ᶜ ∈ F<VAR>haF : 𝓟 {a} ≤ F<VAR>hbG : 𝓟 {b} ≤ G<GOAL>Filter.Tendsto (fun i => if p i then a else b) L (if q then F else G) ↔ ∀ᶠ (i : ι) in L, p i ↔ q
<VAR>α : Type u_1<VAR>A : Set α<VAR>β : Type u_2<VAR>Zero β<VAR>TopologicalSpace β<VAR>ι : Type u_3<VAR>L : Filter ι<VAR>As : ι → Set α<VAR>b : β<VAR>nhd_b : {0}ᶜ ∈ 𝓝 b<VAR>nhd_o : {b}ᶜ ∈ 𝓝 0<VAR>x : α<GOAL>Filter.Tendsto (fun i => (As i).indicator (fun x => b) x) L (𝓝 (A.indicator (fun x => b) x)) ↔ ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A
<VAR>α : Type u_1<VAR>A : Set α<VAR>β : Type u_2<VAR>Zero β<VAR>TopologicalSpace β<VAR>ι : Type u_3<VAR>L : Filter ι<VAR>As : ι → Set α<VAR>b : β<VAR>nhd_b : {0}ᶜ ∈ 𝓝 b<VAR>nhd_o : {b}ᶜ ∈ 𝓝 0<GOAL>Filter.Tendsto (fun i => (As i).indicator fun x => b) L (𝓝 (A.indicator fun x => b)) ↔ ∀ (x : α), ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A
<VAR>α : Type u_1<VAR>A : Set α<VAR>β : Type u_2<VAR>Zero β<VAR>TopologicalSpace β<VAR>ι : Type u_3<VAR>L : Filter ι<VAR>As : ι → Set α<VAR>T1Space β<VAR>b : β<VAR>NeZero b<VAR>x : α<GOAL>Filter.Tendsto (fun i => (As i).indicator (fun x => b) x) L (𝓝 (A.indicator (fun x => b) x)) ↔ ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A
<VAR>α : Type u_1<VAR>A : Set α<VAR>β : Type u_2<VAR>Zero β<VAR>TopologicalSpace β<VAR>ι : Type u_3<VAR>L : Filter ι<VAR>As : ι → Set α<VAR>T1Space β<VAR>b : β<VAR>NeZero b<GOAL>Filter.Tendsto (fun i => (As i).indicator fun x => b) L (𝓝 (A.indicator fun x => b)) ↔ ∀ (x : α), ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A
<VAR>α : Type u_1<VAR>A : Set α<VAR>β : Type u_2<VAR>Zero β<VAR>TopologicalSpace β<VAR>ι : Type u_3<VAR>L : Filter ι<VAR>As : ι → Set α<VAR>b : β<VAR>nhd_b : {0}ᶜ ∈ 𝓝 b<VAR>nhd_o : {b}ᶜ ∈ 𝓝 0<GOAL>Filter.Tendsto (fun i => (As i).indicator fun x => b) L (𝓝 (A.indicator fun x => b)) ↔ Filter.Tendsto As L (Filter.pi fun x => pure (x ∈ A))
<VAR>α : Type u_1<VAR>A : Set α<VAR>β : Type u_2<VAR>Zero β<VAR>TopologicalSpace β<VAR>ι : Type u_3<VAR>L : Filter ι<VAR>As : ι → Set α<VAR>T1Space β<VAR>b : β<VAR>NeZero b<GOAL>Filter.Tendsto (fun i => (As i).indicator fun x => b) L (𝓝 (A.indicator fun x => b)) ↔ Filter.Tendsto As L (Filter.pi fun x => pure (x ∈ A))
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>Z : Type u_5<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>proj : Z → B<VAR>self : Pretrivialization F proj<GOAL>IsOpen self.baseSet
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>Z : Type u_5<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>proj : Z → B<VAR>self : Pretrivialization F proj<GOAL>self.source = proj ⁻¹' self.baseSet
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>Z : Type u_5<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>proj : Z → B<VAR>self : Pretrivialization F proj<GOAL>IsOpen self.target
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>Z : Type u_5<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>proj : Z → B<VAR>self : Pretrivialization F proj<VAR>p : Z<GOAL>p ∈ self.source → (↑self.toPartialEquiv p).1 = proj p
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>Z : Type u_5<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>proj : Z → B<VAR>self : Pretrivialization F proj<GOAL>self.target = self.baseSet ×ˢ Set.univ
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>Z : Type u_5<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>proj : Z → B<VAR>e e' : Pretrivialization F proj<VAR>h₁ : e.toPartialEquiv = e'.toPartialEquiv<VAR>h₂ : e.baseSet = e'.baseSet<GOAL>e = e'
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>Z : Type u_5<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>proj : Z → B<VAR>e e' : Pretrivialization F proj<VAR>h₁ : ∀ (x : Z), ↑e x = ↑e' x<VAR>h₂ : ∀ (x : B × F), ↑e.symm x = ↑e'.symm x<VAR>h₃ : e.baseSet = e'.baseSet<GOAL>e = e'
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>Z : Type u_5<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>proj : Z → B<VAR>Nonempty F<GOAL>Function.Injective Pretrivialization.toPartialEquiv
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>Z : Type u_5<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>proj : Z → B<VAR>e : Pretrivialization F proj<GOAL>↑e.toPartialEquiv = ↑e
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>Z : Type u_5<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>proj : Z → B<VAR>e : Pretrivialization F proj<VAR>x : Z<VAR>ex : x ∈ e.source<GOAL>(↑e x).1 = proj x
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>Z : Type u_5<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>proj : Z → B<VAR>e : Pretrivialization F proj<VAR>x : Z<GOAL>x ∈ e.source ↔ proj x ∈ e.baseSet
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>Z : Type u_5<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>proj : Z → B<VAR>e : Pretrivialization F proj<VAR>x : Z<VAR>ex : proj x ∈ e.baseSet<GOAL>(↑e x).1 = proj x
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>Z : Type u_5<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>proj : Z → B<VAR>e : Pretrivialization F proj<GOAL>Set.EqOn (Prod.fst ∘ ↑e) proj e.source
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>Z : Type u_5<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>proj : Z → B<VAR>e : Pretrivialization F proj<VAR>x : Z<VAR>ex : x ∈ e.source<GOAL>(proj x, (↑e x).2) = ↑e x
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>Z : Type u_5<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>proj : Z → B<VAR>e : Pretrivialization F proj<VAR>x : Z<VAR>ex : proj x ∈ e.baseSet<GOAL>(proj x, (↑e x).2) = ↑e x
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>Z : Type u_5<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>proj : Z → B<VAR>e : Pretrivialization F proj<VAR>x : B × F<GOAL>x ∈ e.target ↔ x.1 ∈ e.baseSet
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>Z : Type u_5<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>proj : Z → B<VAR>e : Pretrivialization F proj<VAR>x : B × F<VAR>hx : x ∈ e.target<GOAL>proj (↑e.symm x) = x.1
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>Z : Type u_5<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>proj : Z → B<VAR>e : Pretrivialization F proj<VAR>b : B<VAR>x : F<VAR>hx : b ∈ e.baseSet<GOAL>proj (↑e.symm (b, x)) = b
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>Z : Type u_5<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>proj : Z → B<VAR>e : Pretrivialization F proj<VAR>Nonempty F<GOAL>Set.SurjOn proj e.source e.baseSet
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>Z : Type u_5<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>proj : Z → B<VAR>e : Pretrivialization F proj<VAR>x : B × F<VAR>hx : x ∈ e.target<GOAL>↑e (↑e.symm x) = x
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>Z : Type u_5<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>proj : Z → B<VAR>e : Pretrivialization F proj<VAR>b : B<VAR>x : F<VAR>hx : b ∈ e.baseSet<GOAL>↑e (↑e.symm (b, x)) = (b, x)
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>Z : Type u_5<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>proj : Z → B<VAR>e : Pretrivialization F proj<VAR>x : Z<VAR>hx : x ∈ e.source<GOAL>↑e.symm (↑e x) = x
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>Z : Type u_5<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>proj : Z → B<VAR>e : Pretrivialization F proj<VAR>x : Z<VAR>ex : x ∈ e.source<GOAL>↑e.symm (proj x, (↑e x).2) = x
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>Z : Type u_5<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>proj : Z → B<VAR>e : Pretrivialization F proj<GOAL>↑e.symm ⁻¹' (proj ⁻¹' e.baseSet) ∩ e.target = e.target
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>Z : Type u_5<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>proj : Z → B<VAR>e : Pretrivialization F proj<VAR>s : Set B<GOAL>↑e.symm ⁻¹' (proj ⁻¹' s) ∩ e.baseSet ×ˢ Set.univ = (s ∩ e.baseSet) ×ˢ Set.univ
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>Z : Type u_5<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>proj : Z → B<VAR>e f : Pretrivialization F proj<GOAL>f.target ∩ ↑f.symm ⁻¹' e.source = (e.baseSet ∩ f.baseSet) ×ˢ Set.univ
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>Z : Type u_5<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>proj : Z → B<VAR>e f : Pretrivialization F proj<GOAL>(f.symm.trans e.toPartialEquiv).source = (e.baseSet ∩ f.baseSet) ×ˢ Set.univ
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>Z : Type u_5<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>proj : Z → B<VAR>e e' : Pretrivialization F proj<GOAL>(e.symm.trans e'.toPartialEquiv).symm = e'.symm.trans e.toPartialEquiv
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>Z : Type u_5<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>proj : Z → B<VAR>e e' : Pretrivialization F proj<GOAL>(e.symm.trans e'.toPartialEquiv).source = (e.baseSet ∩ e'.baseSet) ×ˢ Set.univ
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>Z : Type u_5<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>proj : Z → B<VAR>e e' : Pretrivialization F proj<GOAL>(e.symm.trans e'.toPartialEquiv).target = (e.baseSet ∩ e'.baseSet) ×ˢ Set.univ
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>e' : Pretrivialization F Bundle.TotalSpace.proj<VAR>b : B<VAR>y : E b<GOAL>{ proj := b, snd := y } ∈ e'.source ↔ b ∈ e'.baseSet
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>e' : Pretrivialization F Bundle.TotalSpace.proj<VAR>b : B<VAR>y : E b<VAR>hb : b ∈ e'.baseSet<GOAL>(↑e' { proj := b, snd := y }).1 = b
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>e' : Pretrivialization F Bundle.TotalSpace.proj<VAR>x : B<VAR>y : F<GOAL>(x, y) ∈ e'.target ↔ x ∈ e'.baseSet
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>x : B<VAR>y : F<VAR>e' : Pretrivialization F Bundle.TotalSpace.proj<VAR>h : x ∈ e'.baseSet<GOAL>(↑e'.symm (x, y)).proj = x
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>(x : B) → Zero (E x)<VAR>e : Pretrivialization F Bundle.TotalSpace.proj<VAR>b : B<VAR>hb : b ∈ e.baseSet<VAR>y : F<GOAL>e.symm b y = cast ⋯ (↑e.symm (b, y)).snd
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>(x : B) → Zero (E x)<VAR>e : Pretrivialization F Bundle.TotalSpace.proj<VAR>b : B<VAR>hb : b ∉ e.baseSet<VAR>y : F<GOAL>e.symm b y = 0
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>(x : B) → Zero (E x)<VAR>e : Pretrivialization F Bundle.TotalSpace.proj<VAR>b : B<VAR>hb : b ∉ e.baseSet<GOAL>e.symm b = 0
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>(x : B) → Zero (E x)<VAR>e : Pretrivialization F Bundle.TotalSpace.proj<VAR>b : B<VAR>hb : b ∈ e.baseSet<VAR>y : F<GOAL>{ proj := b, snd := e.symm b y } = ↑e.symm (b, y)
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>(x : B) → Zero (E x)<VAR>e : Pretrivialization F Bundle.TotalSpace.proj<VAR>z : Bundle.TotalSpace F E<VAR>hz : z.proj ∈ e.baseSet<GOAL>e.symm z.proj (↑e z).2 = z.snd
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>(x : B) → Zero (E x)<VAR>e : Pretrivialization F Bundle.TotalSpace.proj<VAR>b : B<VAR>hb : b ∈ e.baseSet<VAR>y : E b<GOAL>e.symm b (↑e { proj := b, snd := y }).2 = y
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>(x : B) → Zero (E x)<VAR>e : Pretrivialization F Bundle.TotalSpace.proj<VAR>b : B<VAR>hb : b ∈ e.baseSet<VAR>y : F<GOAL>↑e { proj := b, snd := e.symm b y } = (b, y)
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>Z : Type u_5<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>TopologicalSpace Z<VAR>proj : Z → B<VAR>self : Trivialization F proj<GOAL>self.source = proj ⁻¹' self.baseSet
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>Z : Type u_5<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>TopologicalSpace Z<VAR>proj : Z → B<VAR>self : Trivialization F proj<VAR>p : Z<GOAL>p ∈ self.source → (↑self.toPartialHomeomorph p).1 = proj p
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>Z : Type u_5<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>TopologicalSpace Z<VAR>proj : Z → B<VAR>self : Trivialization F proj<GOAL>self.target = self.baseSet ×ˢ Set.univ
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>Z : Type u_5<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>TopologicalSpace Z<VAR>proj : Z → B<VAR>self : Trivialization F proj<GOAL>IsOpen self.baseSet
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>Z : Type u_5<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>proj : Z → B<VAR>TopologicalSpace Z<VAR>e e' : Trivialization F proj<VAR>h₁ : e.toPartialHomeomorph = e'.toPartialHomeomorph<VAR>h₂ : e.baseSet = e'.baseSet<GOAL>e = e'
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>Z : Type u_5<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>proj : Z → B<VAR>TopologicalSpace Z<GOAL>Function.Injective fun e => e.toPretrivialization
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>Z : Type u_5<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>proj : Z → B<VAR>TopologicalSpace Z<VAR>e : Trivialization F proj<GOAL>↑e.toPartialHomeomorph = ↑e
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>Z : Type u_5<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>proj : Z → B<VAR>TopologicalSpace Z<VAR>e : Trivialization F proj<VAR>x : Z<VAR>ex : x ∈ e.source<GOAL>(↑e x).1 = proj x
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>Z : Type u_5<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>proj : Z → B<VAR>TopologicalSpace Z<VAR>e : Trivialization F proj<GOAL>Set.EqOn (Prod.fst ∘ ↑e) proj e.source
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>Z : Type u_5<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>proj : Z → B<VAR>TopologicalSpace Z<VAR>e : Trivialization F proj<VAR>x : Z<GOAL>x ∈ e.source ↔ proj x ∈ e.baseSet
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>Z : Type u_5<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>proj : Z → B<VAR>TopologicalSpace Z<VAR>e : Trivialization F proj<VAR>x : Z<VAR>ex : proj x ∈ e.baseSet<GOAL>(↑e x).1 = proj x
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>Z : Type u_5<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>proj : Z → B<VAR>TopologicalSpace Z<VAR>e : Trivialization F proj<VAR>x : Z<VAR>ex : x ∈ e.source<GOAL>(proj x, (↑e x).2) = ↑e x
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>Z : Type u_5<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>proj : Z → B<VAR>TopologicalSpace Z<VAR>e : Trivialization F proj<VAR>x : Z<VAR>ex : proj x ∈ e.baseSet<GOAL>(proj x, (↑e x).2) = ↑e x
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>Z : Type u_5<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>proj : Z → B<VAR>TopologicalSpace Z<VAR>e : Trivialization F proj<VAR>s : Set (B × F)<GOAL>e.source ∩ ↑e ⁻¹' (e.target ∩ s) = e.source ∩ ↑e ⁻¹' s
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>Z : Type u_5<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>proj : Z → B<VAR>TopologicalSpace Z<VAR>e : PartialHomeomorph Z (B × F)<VAR>i : Set B<VAR>j : IsOpen i<VAR>k : e.source = proj ⁻¹' i<VAR>l : e.target = i ×ˢ Set.univ<VAR>m : ∀ p ∈ e.source, (↑e p).1 = proj p<VAR>x : Z<GOAL>↑{ toPartialHomeomorph := e, baseSet := i, open_baseSet := j, source_eq := k, target_eq := l, proj_toFun := m } x = ↑e x
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>Z : Type u_5<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>proj : Z → B<VAR>TopologicalSpace Z<VAR>e : Trivialization F proj<VAR>x : B × F<GOAL>x ∈ e.target ↔ x.1 ∈ e.baseSet
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>Z : Type u_5<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>proj : Z → B<VAR>TopologicalSpace Z<VAR>e : Trivialization F proj<VAR>x : B × F<VAR>hx : x ∈ e.target<GOAL>↑e.symm x ∈ e.source
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>Z : Type u_5<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>proj : Z → B<VAR>TopologicalSpace Z<VAR>e : Trivialization F proj<VAR>x : B × F<VAR>hx : x ∈ e.target<GOAL>proj (↑e.symm x) = x.1
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>Z : Type u_5<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>proj : Z → B<VAR>TopologicalSpace Z<VAR>e : Trivialization F proj<VAR>b : B<VAR>x : F<VAR>hx : b ∈ e.baseSet<GOAL>proj (↑e.symm (b, x)) = b
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>Z : Type u_5<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>proj : Z → B<VAR>TopologicalSpace Z<VAR>e : Trivialization F proj<VAR>Nonempty F<GOAL>Set.SurjOn proj e.source e.baseSet
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>Z : Type u_5<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>proj : Z → B<VAR>TopologicalSpace Z<VAR>e : Trivialization F proj<VAR>x : B × F<VAR>hx : x ∈ e.target<GOAL>↑e (↑e.symm x) = x
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>Z : Type u_5<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>proj : Z → B<VAR>TopologicalSpace Z<VAR>e : Trivialization F proj<VAR>b : B<VAR>x : F<VAR>hx : b ∈ e.baseSet<GOAL>↑e (↑e.symm (b, x)) = (b, x)