ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>UniformSpace α<VAR>UniformSpace β<VAR>ι : Type u_4<VAR>F : ι → β → α<VAR>CompactSpace β<VAR>h : Equicontinuous F<GOAL>UniformEquicontinuous F
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>E : B → Type u_5<VAR>TopologicalSpace (Bundle.TotalSpace F E)<VAR>(b : B) → TopologicalSpace (E b)<VAR>self : FiberBundle F E<VAR>b : B<GOAL>FiberBundle.trivializationAt' b ∈ FiberBundle.trivializationAtlas'
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>E : B → Type u_5<VAR>TopologicalSpace (Bundle.TotalSpace F E)<VAR>(b : B) → TopologicalSpace (E b)<VAR>self : FiberBundle F E<VAR>b : B<GOAL>Inducing (Bundle.TotalSpace.mk b)
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>E : B → Type u_5<VAR>TopologicalSpace (Bundle.TotalSpace F E)<VAR>(b : B) → TopologicalSpace (E b)<VAR>self : FiberBundle F E<VAR>b : B<GOAL>b ∈ (FiberBundle.trivializationAt' b).baseSet
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>E : B → Type u_5<VAR>TopologicalSpace (Bundle.TotalSpace F E)<VAR>(b : B) → TopologicalSpace (E b)<VAR>FiberBundle F E<VAR>b : B<GOAL>Inducing (Bundle.TotalSpace.mk b)
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>E : B → Type u_5<VAR>TopologicalSpace (Bundle.TotalSpace F E)<VAR>(b : B) → TopologicalSpace (E b)<VAR>FiberBundle F E<VAR>b : B<GOAL>b ∈ (trivializationAt F E b).baseSet
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>E : B → Type u_5<VAR>TopologicalSpace (Bundle.TotalSpace F E)<VAR>(b : B) → TopologicalSpace (E b)<VAR>FiberBundle F E<VAR>b : B<GOAL>trivializationAt F E b ∈ trivializationAtlas F E
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>E : B → Type u_5<VAR>TopologicalSpace (Bundle.TotalSpace F E)<VAR>(b : B) → TopologicalSpace (E b)<VAR>FiberBundle F E<VAR>e : Trivialization F Bundle.TotalSpace.proj<VAR>self : MemTrivializationAtlas e<GOAL>e ∈ trivializationAtlas F E
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>E : B → Type u_5<VAR>TopologicalSpace (Bundle.TotalSpace F E)<VAR>(b : B) → TopologicalSpace (E b)<VAR>FiberBundle F E<VAR>e : Trivialization F Bundle.TotalSpace.proj<GOAL>MemTrivializationAtlas e ↔ e ∈ trivializationAtlas F E
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>E : B → Type u_5<VAR>TopologicalSpace (Bundle.TotalSpace F E)<VAR>(b : B) → TopologicalSpace (E b)<VAR>FiberBundle F E<VAR>x : Bundle.TotalSpace F E<GOAL>Filter.map Bundle.TotalSpace.proj (𝓝 x) = 𝓝 x.proj
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>E : B → Type u_5<VAR>TopologicalSpace (Bundle.TotalSpace F E)<VAR>(b : B) → TopologicalSpace (E b)<VAR>FiberBundle F E<GOAL>Continuous Bundle.TotalSpace.proj
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>E : B → Type u_5<VAR>TopologicalSpace (Bundle.TotalSpace F E)<VAR>(b : B) → TopologicalSpace (E b)<VAR>FiberBundle F E<GOAL>IsOpenMap Bundle.TotalSpace.proj
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>E : B → Type u_5<VAR>TopologicalSpace (Bundle.TotalSpace F E)<VAR>(b : B) → TopologicalSpace (E b)<VAR>FiberBundle F E<VAR>Nonempty F<GOAL>Function.Surjective Bundle.TotalSpace.proj
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>E : B → Type u_5<VAR>TopologicalSpace (Bundle.TotalSpace F E)<VAR>(b : B) → TopologicalSpace (E b)<VAR>FiberBundle F E<VAR>Nonempty F<GOAL>QuotientMap Bundle.TotalSpace.proj
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>E : B → Type u_5<VAR>TopologicalSpace (Bundle.TotalSpace F E)<VAR>(b : B) → TopologicalSpace (E b)<VAR>FiberBundle F E<VAR>x : B<GOAL>Continuous (Bundle.TotalSpace.mk x)
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>E : B → Type u_5<VAR>TopologicalSpace (Bundle.TotalSpace F E)<VAR>(b : B) → TopologicalSpace (E b)<VAR>FiberBundle F E<VAR>x : B<GOAL>Embedding (Bundle.TotalSpace.mk x)
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>E : B → Type u_5<VAR>TopologicalSpace (Bundle.TotalSpace F E)<VAR>(b : B) → TopologicalSpace (E b)<VAR>FiberBundle F E<VAR>T1Space B<VAR>x : B<GOAL>ClosedEmbedding (Bundle.TotalSpace.mk x)
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>E : B → Type u_5<VAR>TopologicalSpace (Bundle.TotalSpace F E)<VAR>(b : B) → TopologicalSpace (E b)<VAR>FiberBundle F E<VAR>x : Bundle.TotalSpace F E<GOAL>x ∈ (trivializationAt F E x.proj).source
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>E : B → Type u_5<VAR>TopologicalSpace (Bundle.TotalSpace F E)<VAR>(b : B) → TopologicalSpace (E b)<VAR>FiberBundle F E<VAR>x : Bundle.TotalSpace F E<GOAL>(↑(trivializationAt F E x.proj) x).1 = x.proj
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>X : Type u_4<VAR>TopologicalSpace X<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>E : B → Type u_5<VAR>TopologicalSpace (Bundle.TotalSpace F E)<VAR>(b : B) → TopologicalSpace (E b)<VAR>FiberBundle F E<VAR>f : X → Bundle.TotalSpace F E<VAR>s : Set X<VAR>x₀ : X<GOAL>ContinuousWithinAt f s x₀ ↔ ContinuousWithinAt (fun x => (f x).proj) s x₀ ∧ ContinuousWithinAt (fun x => (↑(trivializationAt F E (f x₀).proj) (f x)).2) s x₀
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>X : Type u_4<VAR>TopologicalSpace X<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>E : B → Type u_5<VAR>TopologicalSpace (Bundle.TotalSpace F E)<VAR>(b : B) → TopologicalSpace (E b)<VAR>FiberBundle F E<VAR>f : X → Bundle.TotalSpace F E<VAR>x₀ : X<GOAL>ContinuousAt f x₀ ↔ ContinuousAt (fun x => (f x).proj) x₀ ∧ ContinuousAt (fun x => (↑(trivializationAt F E (f x₀).proj) (f x)).2) x₀
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>E : B → Type u_5<VAR>TopologicalSpace (Bundle.TotalSpace F E)<VAR>(b : B) → TopologicalSpace (E b)<VAR>ConditionallyCompleteLinearOrder B<VAR>OrderTopology B<VAR>FiberBundle F E<VAR>a b : B<GOAL>∃ e, Set.Icc a b ⊆ e.baseSet
<VAR>ι : Type u_5<VAR>B : Type u_6<VAR>TopologicalSpace B<VAR>F : Type u_7<VAR>TopologicalSpace F<VAR>self : FiberBundleCore ι B F<VAR>i j k : ι<VAR>x : B<GOAL>x ∈ self.baseSet i ∩ self.baseSet j ∩ self.baseSet k → ∀ (v : F), self.coordChange j k x (self.coordChange i j x v) = self.coordChange i k x v
<VAR>ι : Type u_5<VAR>B : Type u_6<VAR>TopologicalSpace B<VAR>F : Type u_7<VAR>TopologicalSpace F<VAR>self : FiberBundleCore ι B F<VAR>i j : ι<GOAL>ContinuousOn (fun p => self.coordChange i j p.1 p.2) ((self.baseSet i ∩ self.baseSet j) ×ˢ Set.univ)
<VAR>ι : Type u_5<VAR>B : Type u_6<VAR>TopologicalSpace B<VAR>F : Type u_7<VAR>TopologicalSpace F<VAR>self : FiberBundleCore ι B F<VAR>i : ι<GOAL>IsOpen (self.baseSet i)
<VAR>ι : Type u_5<VAR>B : Type u_6<VAR>TopologicalSpace B<VAR>F : Type u_7<VAR>TopologicalSpace F<VAR>self : FiberBundleCore ι B F<VAR>i : ι<VAR>x : B<GOAL>x ∈ self.baseSet i → ∀ (v : F), self.coordChange i i x v = v
<VAR>ι : Type u_5<VAR>B : Type u_6<VAR>TopologicalSpace B<VAR>F : Type u_7<VAR>TopologicalSpace F<VAR>self : FiberBundleCore ι B F<VAR>x : B<GOAL>x ∈ self.baseSet (self.indexAt x)
<VAR>ι : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>Z : FiberBundleCore ι B F<VAR>i j : ι<VAR>p : B × F<GOAL>p ∈ (Z.trivChange i j).source ↔ p.1 ∈ Z.baseSet i ∩ Z.baseSet j
<VAR>ι : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>Z : FiberBundleCore ι B F<VAR>i : ι<VAR>p : Z.TotalSpace<GOAL>p ∈ (Z.localTrivAsPartialEquiv i).source ↔ p.proj ∈ Z.baseSet i
<VAR>ι : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>Z : FiberBundleCore ι B F<VAR>i : ι<VAR>p : B × F<GOAL>p ∈ (Z.localTrivAsPartialEquiv i).target ↔ p.1 ∈ Z.baseSet i
<VAR>ι : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>Z : FiberBundleCore ι B F<VAR>i : ι<VAR>p : Z.TotalSpace<GOAL>↑(Z.localTrivAsPartialEquiv i) p = (p.proj, Z.coordChange (Z.indexAt p.proj) i p.proj p.snd)
<VAR>ι : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>Z : FiberBundleCore ι B F<VAR>i j : ι<GOAL>(Z.localTrivAsPartialEquiv i).symm.trans (Z.localTrivAsPartialEquiv j) ≈ (Z.trivChange i j).toPartialEquiv
<VAR>ι : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>Z : FiberBundleCore ι B F<VAR>i : ι<GOAL>IsOpen (Z.localTrivAsPartialEquiv i).source
<VAR>ι : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>Z : FiberBundleCore ι B F<VAR>b : B<GOAL>Z.localTriv (Z.indexAt b) = Z.localTrivAt b
<VAR>ι : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>Z : FiberBundleCore ι B F<VAR>b : B<VAR>p : Bundle.TotalSpace F Z.Fiber<GOAL>(↑(Z.localTrivAt b) p).2 = Z.coordChange (Z.indexAt p.proj) (Z.indexAt b) p.proj p.snd
<VAR>ι : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>Z : FiberBundleCore ι B F<VAR>v : F<VAR>h : ∀ (i j : ι), ∀ x ∈ Z.baseSet i ∩ Z.baseSet j, Z.coordChange i j x v = v<GOAL>Continuous (let_fun this := fun x => { proj := x, snd := v }; this)
<VAR>ι : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>Z : FiberBundleCore ι B F<VAR>i : ι<GOAL>↑(Z.localTrivAsPartialEquiv i) = ↑(Z.localTriv i)
<VAR>ι : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>Z : FiberBundleCore ι B F<VAR>i : ι<GOAL>(Z.localTrivAsPartialEquiv i).source = (Z.localTriv i).source
<VAR>ι : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>Z : FiberBundleCore ι B F<VAR>i : ι<GOAL>(Z.localTrivAsPartialEquiv i).target = (Z.localTriv i).target
<VAR>ι : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>Z : FiberBundleCore ι B F<VAR>i : ι<GOAL>(Z.localTrivAsPartialEquiv i).symm = (Z.localTriv i).symm
<VAR>ι : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>Z : FiberBundleCore ι B F<VAR>i : ι<GOAL>Z.baseSet i = (Z.localTriv i).baseSet
<VAR>ι : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>Z : FiberBundleCore ι B F<VAR>i : ι<VAR>p : Z.TotalSpace<GOAL>↑(Z.localTriv i) p = (p.proj, Z.coordChange (Z.indexAt p.proj) i p.proj p.snd)
<VAR>ι : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>Z : FiberBundleCore ι B F<VAR>p : Z.TotalSpace<GOAL>↑(Z.localTrivAt p.proj) p = (p.proj, p.snd)
<VAR>ι : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>Z : FiberBundleCore ι B F<VAR>b : B<VAR>a : F<GOAL>↑(Z.localTrivAt b) { proj := b, snd := a } = (b, a)
<VAR>ι : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>Z : FiberBundleCore ι B F<VAR>i : ι<VAR>p : Z.TotalSpace<GOAL>p ∈ (Z.localTriv i).source ↔ p.proj ∈ (Z.localTriv i).baseSet
<VAR>ι : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>Z : FiberBundleCore ι B F<VAR>p : Z.TotalSpace<VAR>b : B<GOAL>p ∈ (Z.localTrivAt b).source ↔ p.proj ∈ (Z.localTrivAt b).baseSet
<VAR>ι : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>Z : FiberBundleCore ι B F<VAR>i : ι<VAR>p : B × F<GOAL>p ∈ (Z.localTriv i).target ↔ p.1 ∈ (Z.localTriv i).baseSet
<VAR>ι : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>Z : FiberBundleCore ι B F<VAR>p : B × F<VAR>b : B<GOAL>p ∈ (Z.localTrivAt b).target ↔ p.1 ∈ (Z.localTrivAt b).baseSet
<VAR>ι : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>Z : FiberBundleCore ι B F<VAR>i : ι<VAR>p : B × F<GOAL>↑(Z.localTriv i).symm p = { proj := p.1, snd := Z.coordChange i (Z.indexAt p.1) p.1 p.2 }
<VAR>ι : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>Z : FiberBundleCore ι B F<VAR>b : B<GOAL>b ∈ (Z.localTrivAt b).baseSet
<VAR>ι : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>Z : FiberBundleCore ι B F<VAR>b : B<VAR>a : F<GOAL>{ proj := b, snd := a } ∈ (Z.localTrivAt b).source
<VAR>ι : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>Z : FiberBundleCore ι B F<VAR>b : B<GOAL>Continuous (Bundle.TotalSpace.mk b)
<VAR>ι : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>Z : FiberBundleCore ι B F<GOAL>Continuous Z.proj
<VAR>ι : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>Z : FiberBundleCore ι B F<GOAL>IsOpenMap Z.proj
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_5<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>(x : B) → TopologicalSpace (E x)<VAR>self : FiberPrebundle F E<VAR>b : B<GOAL>Inducing (↑(self.pretrivializationAt b) ∘ Bundle.TotalSpace.mk b)
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_5<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>(x : B) → TopologicalSpace (E x)<VAR>self : FiberPrebundle F E<VAR>e : Pretrivialization F Bundle.TotalSpace.proj<GOAL>e ∈ self.pretrivializationAtlas → ∀ e' ∈ self.pretrivializationAtlas, ContinuousOn (↑e ∘ ↑e'.symm) (e'.target ∩ ↑e'.symm ⁻¹' e.source)
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_5<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>(x : B) → TopologicalSpace (E x)<VAR>self : FiberPrebundle F E<VAR>x : B<GOAL>self.pretrivializationAt x ∈ self.pretrivializationAtlas
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_5<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>(x : B) → TopologicalSpace (E x)<VAR>self : FiberPrebundle F E<VAR>x : B<GOAL>x ∈ (self.pretrivializationAt x).baseSet
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_5<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>(x : B) → TopologicalSpace (E x)<VAR>a : FiberPrebundle F E<VAR>e : Pretrivialization F Bundle.TotalSpace.proj<VAR>he : e ∈ a.pretrivializationAtlas<GOAL>ContinuousOn (↑e.symm) e.target
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_5<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>(x : B) → TopologicalSpace (E x)<VAR>a : FiberPrebundle F E<VAR>e : Pretrivialization F Bundle.TotalSpace.proj<GOAL>IsOpen e.source
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_5<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>(x : B) → TopologicalSpace (E x)<VAR>a : FiberPrebundle F E<VAR>e e' : Pretrivialization F Bundle.TotalSpace.proj<VAR>he' : e' ∈ a.pretrivializationAtlas<GOAL>IsOpen (e'.target ∩ ↑e'.symm ⁻¹' e.source)
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_5<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>(x : B) → TopologicalSpace (E x)<VAR>a : FiberPrebundle F E<VAR>b : B<VAR>x : E b<GOAL>{ proj := b, snd := x } ∈ (a.pretrivializationAt b).source
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_5<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>(x : B) → TopologicalSpace (E x)<VAR>a : FiberPrebundle F E<VAR>b : B<GOAL>Bundle.TotalSpace.mk b ⁻¹' (a.pretrivializationAt b).source = Set.univ
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_5<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>(x : B) → TopologicalSpace (E x)<VAR>a : FiberPrebundle F E<VAR>b : B<GOAL>Continuous (Bundle.TotalSpace.mk b)
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_5<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>(x : B) → TopologicalSpace (E x)<VAR>a : FiberPrebundle F E<VAR>b : B<VAR>h : Inducing (↑(a.pretrivializationAt b) ∘ Bundle.TotalSpace.mk b)<GOAL>Inducing (Bundle.TotalSpace.mk b)
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_5<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>(x : B) → TopologicalSpace (E x)<VAR>a : FiberPrebundle F E<GOAL>Continuous Bundle.TotalSpace.proj
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_5<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>(x : B) → TopologicalSpace (E x)<VAR>a : FiberPrebundle F E<VAR>X : Type u_6<VAR>TopologicalSpace X<VAR>f : Bundle.TotalSpace F E → X<VAR>s : Set B<VAR>hs : IsOpen s<VAR>hf : ∀ b ∈ s, ContinuousOn (f ∘ ↑(a.pretrivializationAt b).symm) ((s ∩ (a.pretrivializationAt b).baseSet) ×ˢ Set.univ)<GOAL>ContinuousOn f (Bundle.TotalSpace.proj ⁻¹' s)
<VAR>α : Type u<VAR>UniformSpace α<VAR>ι : Sort u_1<VAR>p : ι → Prop<VAR>s : ι → Set (α × α)<VAR>h : (𝓤 α).HasBasis p s<VAR>x y : α<GOAL>x ⤳ y ↔ ∀ (i : ι), p i → (x, y) ∈ s i
<VAR>α : Type u<VAR>UniformSpace α<VAR>ι : Sort u_1<VAR>p : ι → Prop<VAR>s : ι → Set (α × α)<VAR>h : (𝓤 α).HasBasis p s<VAR>x y : α<GOAL>Inseparable x y ↔ ∀ (i : ι), p i → (x, y) ∈ s i
<VAR>α : Type u<VAR>UniformSpace α<VAR>x y : α<GOAL>Inseparable x y ↔ (x, y) ∈ (𝓤 α).ker
<VAR>α : Type u<VAR>UniformSpace α<VAR>x y : α<VAR>h : Inseparable x y<GOAL>𝓝 (x, y) ≤ 𝓤 α
<VAR>α : Type u<VAR>UniformSpace α<VAR>x y : α<GOAL>Inseparable x y ↔ ClusterPt (x, y) (𝓤 α)
<VAR>α : Type u<VAR>UniformSpace α<GOAL>T0Space α ↔ ∀ (x y : α), (∀ r ∈ 𝓤 α, (x, y) ∈ r) → x = y
<VAR>α : Type u<VAR>UniformSpace α<GOAL>T0Space α ↔ Pairwise fun x y => ∃ r ∈ 𝓤 α, (x, y) ∉ r
<VAR>α : Type u<VAR>UniformSpace α<GOAL>T0Space α ↔ (𝓤 α).ker = Set.diagonal α
<VAR>α : Type u_1<VAR>UniformSpace α<VAR>T0Space α<VAR>x y : α<VAR>h : ∀ {V : Set (α × α)}, V ∈ 𝓤 α → (x, y) ∈ V<GOAL>x = y
<VAR>α : Type u_1<VAR>UniformSpace α<VAR>T0Space α<VAR>ι : Sort u_2<VAR>p : ι → Prop<VAR>s : ι → Set (α × α)<VAR>hs : (𝓤 α).HasBasis p s<VAR>x y : α<VAR>h : ∀ {i : ι}, p i → (x, y) ∈ s i<GOAL>x = y
<VAR>α : Type u_1<VAR>UniformSpace α<VAR>T0Space α<VAR>x y : α<VAR>h : ∀ {V : Set (α × α)}, V ∈ 𝓤 α → SymmetricRel V → (x, y) ∈ V<GOAL>x = y
<VAR>α : Type u<VAR>UniformSpace α<VAR>T0Space α<VAR>x y : α<VAR>h : ClusterPt (x, y) (𝓤 α)<GOAL>x = y
<VAR>α : Type u<VAR>β : Type v<VAR>UniformSpace α<VAR>l : Filter β<VAR>l.NeBot<VAR>f g : β → α<VAR>a b : α<VAR>ha : Filter.Tendsto f l (𝓝 a)<VAR>hb : Filter.Tendsto g l (𝓝 b)<GOAL>Inseparable a b ↔ Filter.Tendsto (fun x => (f x, g x)) l (𝓤 α)
<VAR>α : Type u<VAR>UniformSpace α<VAR>T0Space α<VAR>V₀ : Set (α × α)<VAR>V₀_in : V₀ ∈ 𝓤 α<VAR>s : Set α<VAR>hs : s.Pairwise fun x y => (x, y) ∉ V₀<GOAL>IsClosed s
<VAR>α : Type u<VAR>UniformSpace α<VAR>ι : Type u_1<VAR>T0Space α<VAR>V₀ : Set (α × α)<VAR>V₀_in : V₀ ∈ 𝓤 α<VAR>f : ι → α<VAR>hf : Pairwise fun x y => (f x, f y) ∉ V₀<GOAL>IsClosed (Set.range f)
<VAR>α : Type u<VAR>UniformSpace α<GOAL>Filter.comap (Prod.map SeparationQuotient.mk SeparationQuotient.mk) (Filter.map (Prod.map SeparationQuotient.mk SeparationQuotient.mk) (𝓤 α)) = 𝓤 α
<VAR>α : Type u<VAR>UniformSpace α<GOAL>𝓤 (SeparationQuotient α) = Filter.map (Prod.map SeparationQuotient.mk SeparationQuotient.mk) (𝓤 α)
<VAR>α : Type u<VAR>UniformSpace α<GOAL>UniformContinuous SeparationQuotient.mk
<VAR>α : Type u<VAR>β : Type v<VAR>UniformSpace α<VAR>UniformSpace β<VAR>f : SeparationQuotient α → β<GOAL>UniformContinuous f ↔ UniformContinuous (f ∘ SeparationQuotient.mk)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>UniformSpace α<VAR>UniformSpace β<VAR>UniformSpace γ<VAR>f : SeparationQuotient α × SeparationQuotient β → γ<GOAL>UniformContinuous f ↔ UniformContinuous fun p => f (SeparationQuotient.mk p.1, SeparationQuotient.mk p.2)
<VAR>α : Type u<VAR>β : Type v<VAR>UniformSpace α<VAR>UniformSpace β<VAR>f : α → β<VAR>h : ∀ (a b : α), Inseparable a b → f a = f b<GOAL>UniformContinuous (SeparationQuotient.lift f h) ↔ UniformContinuous f
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>UniformSpace α<VAR>UniformSpace β<VAR>UniformSpace γ<VAR>f : α → β → γ<VAR>h : ∀ (a : α) (c : β) (b : α) (d : β), Inseparable a b → Inseparable c d → f a c = f b d<GOAL>UniformContinuous (Function.uncurry (SeparationQuotient.lift₂ f h)) ↔ UniformContinuous (Function.uncurry f)
<VAR>α : Type u<VAR>UniformSpace α<GOAL>Filter.comap (Prod.map SeparationQuotient.mk SeparationQuotient.mk) (𝓤 (SeparationQuotient α)) = 𝓤 α
<VAR>α : Type u<VAR>β : Type v<VAR>UniformSpace α<VAR>UniformSpace β<VAR>T0Space β<VAR>f : α → β<VAR>h : UniformContinuous f<VAR>a : α<GOAL>SeparationQuotient.lift' f (SeparationQuotient.mk a) = f a
<VAR>α : Type u<VAR>β : Type v<VAR>UniformSpace α<VAR>UniformSpace β<VAR>T0Space β<VAR>f : α → β<GOAL>UniformContinuous (SeparationQuotient.lift' f)
<VAR>α : Type u<VAR>β : Type v<VAR>UniformSpace α<VAR>UniformSpace β<VAR>f : α → β<VAR>h : UniformContinuous f<VAR>a : α<GOAL>SeparationQuotient.map f (SeparationQuotient.mk a) = SeparationQuotient.mk (f a)
<VAR>α : Type u<VAR>β : Type v<VAR>UniformSpace α<VAR>UniformSpace β<VAR>f : α → β<GOAL>UniformContinuous (SeparationQuotient.map f)
<VAR>α : Type u<VAR>β : Type v<VAR>UniformSpace α<VAR>UniformSpace β<VAR>f : α → β<VAR>hf : UniformContinuous f<VAR>g : SeparationQuotient α → SeparationQuotient β<VAR>comm : SeparationQuotient.mk ∘ f = g ∘ SeparationQuotient.mk<GOAL>SeparationQuotient.map f = g
<VAR>α : Type u<VAR>UniformSpace α<GOAL>SeparationQuotient.map id = id
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>UniformSpace α<VAR>UniformSpace β<VAR>UniformSpace γ<VAR>f : α → β<VAR>g : β → γ<VAR>hf : UniformContinuous f<VAR>hg : UniformContinuous g<GOAL>SeparationQuotient.map g ∘ SeparationQuotient.map f = SeparationQuotient.map (g ∘ f)
<VAR>α : Type u<VAR>UniformSpace α<GOAL>Monotone CauchyFilter.gen
<VAR>α : Type u<VAR>UniformSpace α<GOAL>Filter.map Prod.swap ((𝓤 α).lift' CauchyFilter.gen) ≤ (𝓤 α).lift' CauchyFilter.gen
<VAR>α : Type u<VAR>UniformSpace α<VAR>s t : Set (α × α)<GOAL>CauchyFilter.gen s ○ CauchyFilter.gen t ⊆ CauchyFilter.gen (s ○ t)
<VAR>α : Type u<VAR>UniformSpace α<GOAL>(((𝓤 α).lift' CauchyFilter.gen).lift' fun s => s ○ s) ≤ (𝓤 α).lift' CauchyFilter.gen
<VAR>α : Type u<VAR>UniformSpace α<VAR>s : Set (CauchyFilter α × CauchyFilter α)<GOAL>s ∈ 𝓤 (CauchyFilter α) ↔ ∃ t ∈ 𝓤 α, CauchyFilter.gen t ⊆ s
<VAR>α : Type u<VAR>UniformSpace α<VAR>ι : Sort u_1<VAR>p : ι → Prop<VAR>s : ι → Set (α × α)<VAR>h : (𝓤 α).HasBasis p s<GOAL>(𝓤 (CauchyFilter α)).HasBasis p (CauchyFilter.gen ∘ s)
<VAR>α : Type u<VAR>UniformSpace α<VAR>s : Set (CauchyFilter α × CauchyFilter α)<GOAL>s ∈ 𝓤 (CauchyFilter α) ↔ ∃ t ∈ 𝓤 α, ∀ (f g : CauchyFilter α), t ∈ ↑f ×ˢ ↑g → (f, g) ∈ s
<VAR>α : Type u<VAR>UniformSpace α<GOAL>UniformInducing CauchyFilter.pureCauchy
<VAR>α : Type u<VAR>UniformSpace α<GOAL>UniformEmbedding CauchyFilter.pureCauchy
<VAR>α : Type u<VAR>UniformSpace α<GOAL>DenseRange CauchyFilter.pureCauchy
<VAR>α : Type u<VAR>UniformSpace α<GOAL>DenseInducing CauchyFilter.pureCauchy
<VAR>α : Type u<VAR>UniformSpace α<GOAL>DenseEmbedding CauchyFilter.pureCauchy
<VAR>α : Type u<VAR>UniformSpace α<GOAL>Nonempty (CauchyFilter α) ↔ Nonempty α
<VAR>α : Type u<VAR>UniformSpace α<VAR>β : Type v<VAR>UniformSpace β<VAR>T0Space β<VAR>f : α → β<VAR>hf : UniformContinuous f<VAR>a : α<GOAL>CauchyFilter.extend f (CauchyFilter.pureCauchy a) = f a
<VAR>α : Type u<VAR>UniformSpace α<VAR>β : Type v<VAR>UniformSpace β<VAR>CompleteSpace β<VAR>f : α → β<GOAL>UniformContinuous (CauchyFilter.extend f)
<VAR>α : Type u<VAR>UniformSpace α<VAR>f g : CauchyFilter α<GOAL>Inseparable f g ↔ ↑f ×ˢ ↑g ≤ 𝓤 α
<VAR>α : Type u<VAR>UniformSpace α<VAR>f g : CauchyFilter α<VAR>a b : α<VAR>ha : ↑f ≤ 𝓝 a<VAR>hb : ↑g ≤ 𝓝 b<GOAL>Inseparable a b ↔ Inseparable f g
<VAR>α : Type u<VAR>UniformSpace α<VAR>CompleteSpace α<VAR>f g : CauchyFilter α<GOAL>Inseparable (lim ↑f) (lim ↑g) ↔ Inseparable f g
<VAR>α : Type u_1<VAR>UniformSpace α<VAR>CompleteSpace α<VAR>T0Space α<VAR>f g : CauchyFilter α<GOAL>lim ↑f = lim ↑g ↔ Inseparable f g
<VAR>α : Type u_1<VAR>UniformSpace α<VAR>T0Space α<GOAL>Function.Injective fun a => SeparationQuotient.mk (CauchyFilter.pureCauchy a)
<VAR>α : Type u_1<VAR>UniformSpace α<GOAL>↑α = SeparationQuotient.mk ∘ CauchyFilter.pureCauchy
<VAR>α : Type u_1<VAR>UniformSpace α<GOAL>UniformInducing ↑α
<VAR>α : Type u_1<VAR>UniformSpace α<GOAL>Filter.comap (fun p => (↑α p.1, ↑α p.2)) (𝓤 (UniformSpace.Completion α)) = 𝓤 α
<VAR>α : Type u_1<VAR>UniformSpace α<GOAL>DenseRange ↑α
<VAR>α : Type u_1<VAR>UniformSpace α<GOAL>Nonempty (UniformSpace.Completion α) ↔ Nonempty α