ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>x : α<VAR>y : β<VAR>r : ℝ≥0∞<GOAL>EMetric.closedBall x r ×ˢ EMetric.closedBall y r = EMetric.closedBall (x, y) r
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>x : α<VAR>s : Set α<GOAL>x ∈ closure s ↔ ∀ ε > 0, ∃ y ∈ s, edist x y < ε
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoEMetricSpace α<VAR>f : Filter β<VAR>u : β → α<VAR>a : α<GOAL>Filter.Tendsto u f (𝓝 a) ↔ ∀ ε > 0, ∀ᶠ (x : β) in f, edist (u x) a < ε
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoEMetricSpace α<VAR>Nonempty β<VAR>SemilatticeSup β<VAR>u : β → α<VAR>a : α<GOAL>Filter.Tendsto u Filter.atTop (𝓝 a) ↔ ∀ ε > 0, ∃ N, ∀ n ≥ N, edist (u n) a < ε
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>x y : α<GOAL>Inseparable x y ↔ edist x y = 0
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoEMetricSpace α<VAR>Nonempty β<VAR>SemilatticeSup β<VAR>u : β → α<GOAL>CauchySeq u ↔ ∀ ε > 0, ∃ N, ∀ (m : β), N ≤ m → ∀ (n : β), N ≤ n → edist (u m) (u n) < ε
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoEMetricSpace α<VAR>Nonempty β<VAR>SemilatticeSup β<VAR>u : β → α<GOAL>CauchySeq u ↔ ∀ ε > 0, ∃ N, ∀ n ≥ N, edist (u n) (u N) < ε
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoEMetricSpace α<VAR>Nonempty β<VAR>SemilatticeSup β<VAR>u : β → α<GOAL>CauchySeq u ↔ ∀ (ε : ℝ≥0), 0 < ε → ∃ N, ∀ (n : β), N ≤ n → edist (u n) (u N) < ↑ε
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>s : Set α<GOAL>TotallyBounded s ↔ ∀ ε > 0, ∃ t, t.Finite ∧ s ⊆ ⋃ y ∈ t, EMetric.ball y ε
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>s : Set α<GOAL>TotallyBounded s ↔ ∀ ε > 0, ∃ t ⊆ s, t.Finite ∧ s ⊆ ⋃ y ∈ t, EMetric.ball y ε
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>s : Set α<VAR>hs : ∀ ε > 0, ∃ t, t.Countable ∧ s ⊆ ⋃ x ∈ t, EMetric.closedBall x ε<GOAL>∃ t ⊆ s, t.Countable ∧ s ⊆ closure t
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>s : Set α<VAR>hs : TopologicalSpace.IsSeparable s<GOAL>∃ t ⊆ s, t.Countable ∧ s ⊆ closure t
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>s : Set α<VAR>hs : TopologicalSpace.IsSeparable s<GOAL>TopologicalSpace.SeparableSpace ↑s
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>s : Set α<VAR>hs : IsCompact s<GOAL>∃ t ⊆ s, t.Countable ∧ s ⊆ closure t
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>hs : ∀ ε > 0, ∃ t, t.Countable ∧ ⋃ x ∈ t, EMetric.closedBall x ε = Set.univ<GOAL>SecondCountableTopology α
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>s : Set α<GOAL>EMetric.diam s = sSup (Set.image2 edist s s)
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>s : Set α<VAR>d : ℝ≥0∞<GOAL>EMetric.diam s ≤ d ↔ ∀ x ∈ s, ∀ y ∈ s, edist x y ≤ d
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoEMetricSpace α<VAR>d : ℝ≥0∞<VAR>f : β → α<VAR>s : Set β<GOAL>EMetric.diam (f '' s) ≤ d ↔ ∀ x ∈ s, ∀ y ∈ s, edist (f x) (f y) ≤ d
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>x y : α<VAR>s : Set α<VAR>d : ℝ≥0∞<VAR>hx : x ∈ s<VAR>hy : y ∈ s<VAR>hd : EMetric.diam s ≤ d<GOAL>edist x y ≤ d
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>x y : α<VAR>s : Set α<VAR>hx : x ∈ s<VAR>hy : y ∈ s<GOAL>edist x y ≤ EMetric.diam s
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>s : Set α<VAR>d : ℝ≥0∞<VAR>h : ∀ x ∈ s, ∀ y ∈ s, edist x y ≤ d<GOAL>EMetric.diam s ≤ d
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>s : Set α<VAR>hs : s.Subsingleton<GOAL>EMetric.diam s = 0
<VAR>α : Type u<VAR>PseudoEMetricSpace α<GOAL>EMetric.diam ∅ = 0
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>x : α<GOAL>EMetric.diam {x} = 0
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>Zero α<GOAL>EMetric.diam 0 = 0
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>One α<GOAL>EMetric.diam 1 = 0
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>ι : Type u_2<VAR>o : Option ι<VAR>s : ι → Set α<GOAL>EMetric.diam (⋃ i ∈ o, s i) = ⨆ i ∈ o, EMetric.diam (s i)
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>x : α<VAR>s : Set α<GOAL>EMetric.diam (insert x s) = max (⨆ y ∈ s, edist x y) (EMetric.diam s)
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>x y : α<GOAL>EMetric.diam {x, y} = edist x y
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>x y z : α<GOAL>EMetric.diam {x, y, z} = max (max (edist x y) (edist x z)) (edist y z)
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>s t : Set α<VAR>h : s ⊆ t<GOAL>EMetric.diam s ≤ EMetric.diam t
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>x y : α<VAR>s t : Set α<VAR>xs : x ∈ s<VAR>yt : y ∈ t<GOAL>EMetric.diam (s ∪ t) ≤ EMetric.diam s + edist x y + EMetric.diam t
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>s t : Set α<VAR>h : (s ∩ t).Nonempty<GOAL>EMetric.diam (s ∪ t) ≤ EMetric.diam s + EMetric.diam t
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>x : α<VAR>r : ℝ≥0∞<GOAL>EMetric.diam (EMetric.closedBall x r) ≤ 2 * r
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>x : α<VAR>r : ℝ≥0∞<GOAL>EMetric.diam (EMetric.ball x r) ≤ 2 * r
<VAR>β : Type v<VAR>π : β → Type u_2<VAR>Fintype β<VAR>(b : β) → PseudoEMetricSpace (π b)<VAR>s : (b : β) → Set (π b)<VAR>c : ℝ≥0∞<VAR>h : ∀ (b : β), EMetric.diam (s b) ≤ c<GOAL>EMetric.diam (Set.univ.pi s) ≤ c
<VAR>α : Type u<VAR>self : EMetricSpace α<VAR>x y : α<GOAL>edist x y = 0 → x = y
<VAR>α : Type u_2<VAR>m m' : EMetricSpace α<VAR>h : PseudoEMetricSpace.toEDist = PseudoEMetricSpace.toEDist<GOAL>m = m'
<VAR>γ : Type w<VAR>EMetricSpace γ<VAR>x y : γ<GOAL>edist x y = 0 ↔ x = y
<VAR>γ : Type w<VAR>EMetricSpace γ<VAR>x y : γ<GOAL>0 = edist x y ↔ x = y
<VAR>γ : Type w<VAR>EMetricSpace γ<VAR>x y : γ<GOAL>edist x y ≤ 0 ↔ x = y
<VAR>γ : Type w<VAR>EMetricSpace γ<VAR>x y : γ<GOAL>0 < edist x y ↔ x ≠ y
<VAR>γ : Type w<VAR>EMetricSpace γ<VAR>x y : γ<VAR>h : ∀ ε > 0, edist x y ≤ ε<GOAL>x = y
<VAR>β : Type v<VAR>γ : Type w<VAR>EMetricSpace γ<VAR>EMetricSpace β<VAR>f : γ → β<GOAL>UniformEmbedding f ↔ (∀ ε > 0, ∃ δ > 0, ∀ {a b : γ}, edist a b < δ → edist (f a) (f b) < ε) ∧ ∀ δ > 0, ∃ ε > 0, ∀ {a b : γ}, edist (f a) (f b) < ε → edist a b < δ
<VAR>γ : Type w<VAR>EMetricSpace γ<GOAL>𝓤 γ = ⨅ ε, ⨅ (_ : ε > 0), 𝓟 {p | edist p.1 p.2 < ε}
<VAR>γ : Type w<VAR>EMetricSpace γ<VAR>s : Set γ<VAR>hs : IsCompact s<GOAL>∃ t ⊆ s, t.Countable ∧ s = closure t
<VAR>γ : Type w<VAR>EMetricSpace γ<VAR>s : Set γ<GOAL>EMetric.diam s = 0 ↔ s.Subsingleton
<VAR>γ : Type w<VAR>EMetricSpace γ<VAR>s : Set γ<GOAL>0 < EMetric.diam s ↔ s.Nontrivial
<VAR>γ : Type w<VAR>EMetricSpace γ<VAR>s : Set γ<GOAL>0 < EMetric.diam s ↔ ∃ x ∈ s, ∃ y ∈ s, x ≠ y
<VAR>X : Type u_1<VAR>PseudoEMetricSpace X<VAR>x y : X<GOAL>edist (SeparationQuotient.mk x) (SeparationQuotient.mk y) = edist x y
<VAR>X : Type u_1<VAR>EDist X<VAR>a b : X<GOAL>edist (Additive.ofMul a) (Additive.ofMul b) = edist a b
<VAR>X : Type u_1<VAR>EDist X<VAR>a b : X<GOAL>edist (Multiplicative.ofAdd a) (Multiplicative.ofAdd b) = edist a b
<VAR>X : Type u_1<VAR>EDist X<VAR>a b : Additive X<GOAL>edist (Additive.toMul a) (Additive.toMul b) = edist a b
<VAR>X : Type u_1<VAR>EDist X<VAR>a b : Multiplicative X<GOAL>edist (Multiplicative.toAdd a) (Multiplicative.toAdd b) = edist a b
<VAR>X : Type u_1<VAR>EDist X<VAR>a b : X<GOAL>edist (OrderDual.toDual a) (OrderDual.toDual b) = edist a b
<VAR>X : Type u_1<VAR>EDist X<VAR>a b : Xᵒᵈ<GOAL>edist (OrderDual.ofDual a) (OrderDual.ofDual b) = edist a b
<VAR>B : Type u_1<VAR>F : Type u_2<VAR>Z : Type u_3<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>TopologicalSpace Z<VAR>proj : Z → B<VAR>h : IsHomeomorphicTrivialFiberBundle F proj<GOAL>∃ e, proj = Prod.fst ∘ ⇑e
<VAR>B : Type u_1<VAR>F : Type u_2<VAR>Z : Type u_3<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>TopologicalSpace Z<VAR>proj : Z → B<VAR>Nonempty F<VAR>h : IsHomeomorphicTrivialFiberBundle F proj<GOAL>Function.Surjective proj
<VAR>B : Type u_1<VAR>F : Type u_2<VAR>Z : Type u_3<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>TopologicalSpace Z<VAR>proj : Z → B<VAR>h : IsHomeomorphicTrivialFiberBundle F proj<GOAL>Continuous proj
<VAR>B : Type u_1<VAR>F : Type u_2<VAR>Z : Type u_3<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>TopologicalSpace Z<VAR>proj : Z → B<VAR>h : IsHomeomorphicTrivialFiberBundle F proj<GOAL>IsOpenMap proj
<VAR>B : Type u_1<VAR>F : Type u_2<VAR>Z : Type u_3<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>TopologicalSpace Z<VAR>proj : Z → B<VAR>Nonempty F<VAR>h : IsHomeomorphicTrivialFiberBundle F proj<GOAL>QuotientMap proj
<VAR>B : Type u_1<VAR>F : Type u_2<VAR>TopologicalSpace B<VAR>TopologicalSpace F<GOAL>IsHomeomorphicTrivialFiberBundle F Prod.fst
<VAR>B : Type u_1<VAR>F : Type u_2<VAR>TopologicalSpace B<VAR>TopologicalSpace F<GOAL>IsHomeomorphicTrivialFiberBundle F Prod.snd
<VAR>P : TopCat → Prop<VAR>α : Type w<VAR>Finite α<VAR>X : α → CompHausLike P<VAR>CompHausLike.HasExplicitFiniteCoproduct X<VAR>B : CompHausLike P<VAR>e : (a : α) → X a ⟶ B<VAR>a : α<GOAL>CategoryTheory.CategoryStruct.comp (CompHausLike.finiteCoproduct.ι X a) (CompHausLike.finiteCoproduct.desc X e) = e a
<VAR>P : TopCat → Prop<VAR>α : Type w<VAR>Finite α<VAR>X : α → CompHausLike P<VAR>CompHausLike.HasExplicitFiniteCoproduct X<VAR>B : CompHausLike P<VAR>f g : CompHausLike.finiteCoproduct X ⟶ B<VAR>h : ∀ (a : α), CategoryTheory.CategoryStruct.comp (CompHausLike.finiteCoproduct.ι X a) f = CategoryTheory.CategoryStruct.comp (CompHausLike.finiteCoproduct.ι X a) g<GOAL>f = g
<VAR>P : TopCat → Prop<VAR>α : Type w<VAR>Finite α<VAR>X : α → CompHausLike P<VAR>CompHausLike.HasExplicitFiniteCoproduct X<VAR>a : α<GOAL>Function.Injective ⇑(CompHausLike.finiteCoproduct.ι X a)
<VAR>P : TopCat → Prop<VAR>α : Type w<VAR>Finite α<VAR>X : α → CompHausLike P<VAR>CompHausLike.HasExplicitFiniteCoproduct X<VAR>R : ↑(CompHausLike.finiteCoproduct X).toTop<GOAL>∃ a r, R = (CompHausLike.finiteCoproduct.ι X a) r
<VAR>P : TopCat → Prop<VAR>α : Type w<VAR>Finite α<VAR>X : α → CompHausLike P<VAR>CompHausLike.HasExplicitFiniteCoproduct X<VAR>B : CompHausLike P<VAR>π : (a : α) → X a ⟶ B<VAR>a : α<VAR>x : (CategoryTheory.forget (CompHausLike P)).obj (X a)<GOAL>(CompHausLike.finiteCoproduct.desc X π) ((CompHausLike.finiteCoproduct.ι X a) x) = (π a) x
<VAR>P : TopCat → Prop<VAR>self : CompHausLike.HasExplicitFiniteCoproducts P<VAR>α : Type w<VAR>Finite α<VAR>X : α → CompHausLike P<GOAL>CompHausLike.HasExplicitFiniteCoproduct X
<VAR>P : TopCat → Prop<VAR>α : Type w<VAR>Finite α<VAR>X : α → CompHausLike P<VAR>CompHausLike.HasExplicitFiniteCoproduct X<VAR>a : α<GOAL>OpenEmbedding ⇑(CompHausLike.finiteCoproduct.ι X a)
<VAR>P : TopCat → Prop<VAR>α : Type w<VAR>Finite α<VAR>X : α → CompHausLike P<VAR>CompHausLike.HasExplicitFiniteCoproduct X<VAR>a : α<GOAL>OpenEmbedding ⇑(CategoryTheory.Limits.Sigma.ι X a)
<VAR>P : TopCat → Prop<VAR>X Y B : CompHausLike P<VAR>f : X ⟶ B<VAR>g : Y ⟶ B<VAR>CompHausLike.HasExplicitPullback f g<GOAL>CategoryTheory.CategoryStruct.comp (CompHausLike.pullback.fst f g) f = CategoryTheory.CategoryStruct.comp (CompHausLike.pullback.snd f g) g
<VAR>P : TopCat → Prop<VAR>X Y B : CompHausLike P<VAR>f : X ⟶ B<VAR>g : Y ⟶ B<VAR>CompHausLike.HasExplicitPullback f g<VAR>Z : CompHausLike P<VAR>a : Z ⟶ X<VAR>b : Z ⟶ Y<VAR>w : CategoryTheory.CategoryStruct.comp a f = CategoryTheory.CategoryStruct.comp b g<GOAL>CategoryTheory.CategoryStruct.comp (CompHausLike.pullback.lift f g a b w) (CompHausLike.pullback.fst f g) = a
<VAR>P : TopCat → Prop<VAR>X Y B : CompHausLike P<VAR>f : X ⟶ B<VAR>g : Y ⟶ B<VAR>CompHausLike.HasExplicitPullback f g<VAR>Z : CompHausLike P<VAR>a : Z ⟶ X<VAR>b : Z ⟶ Y<VAR>w : CategoryTheory.CategoryStruct.comp a f = CategoryTheory.CategoryStruct.comp b g<GOAL>CategoryTheory.CategoryStruct.comp (CompHausLike.pullback.lift f g a b w) (CompHausLike.pullback.snd f g) = b
<VAR>P : TopCat → Prop<VAR>X Y B : CompHausLike P<VAR>f : X ⟶ B<VAR>g : Y ⟶ B<VAR>CompHausLike.HasExplicitPullback f g<VAR>Z : CompHausLike P<VAR>a b : Z ⟶ CompHausLike.pullback f g<VAR>hfst : CategoryTheory.CategoryStruct.comp a (CompHausLike.pullback.fst f g) = CategoryTheory.CategoryStruct.comp b (CompHausLike.pullback.fst f g)<VAR>hsnd : CategoryTheory.CategoryStruct.comp a (CompHausLike.pullback.snd f g) = CategoryTheory.CategoryStruct.comp b (CompHausLike.pullback.snd f g)<GOAL>a = b
<VAR>P : TopCat → Prop<VAR>X Y B : CompHausLike P<VAR>f : X ⟶ B<VAR>g : Y ⟶ B<VAR>CompHausLike.HasExplicitPullback f g<GOAL>(CompHausLike.pullback.cone f g).π = { app := fun j => Option.rec (CategoryTheory.CategoryStruct.comp (CompHausLike.pullback.fst f g) f) (fun val => CategoryTheory.Limits.WalkingPair.rec (CompHausLike.pullback.fst f g) (CompHausLike.pullback.snd f g) val) j, naturality := ⋯ }
<VAR>P : TopCat → Prop<VAR>X Y B : CompHausLike P<VAR>f : X ⟶ B<VAR>g : Y ⟶ B<VAR>CompHausLike.HasExplicitPullback f g<GOAL>(CompHausLike.pullback.cone f g).pt = CompHausLike.pullback f g
<VAR>P : TopCat → Prop<VAR>X Y B : CompHausLike P<VAR>f : X ⟶ B<VAR>g : Y ⟶ B<VAR>CompHausLike.HasExplicitPullback f g<VAR>s : CategoryTheory.Limits.PullbackCone f g<GOAL>(CompHausLike.pullback.isLimit f g).lift s = CompHausLike.pullback.lift f g s.fst s.snd ⋯
<VAR>P : TopCat → Prop<VAR>self : CompHausLike.HasExplicitPullbacks P<VAR>X Y B : CompHausLike P<VAR>f : X ⟶ B<VAR>g : Y ⟶ B<GOAL>CompHausLike.HasExplicitPullback f g
<VAR>P : TopCat → Prop<VAR>CompHausLike.HasExplicitFiniteCoproducts P<VAR>self : CompHausLike.HasExplicitPullbacksOfInclusions P<VAR>X Y Z : CompHausLike P<VAR>f : Z ⟶ X ⨿ Y<GOAL>CompHausLike.HasExplicitPullback CategoryTheory.Limits.coprod.inl f
<VAR>P : TopCat → Prop<VAR>CompHausLike.HasExplicitFiniteCoproducts P<VAR>hP' : ∀ ⦃X Y B : CompHausLike P⦄ (f : X ⟶ B) (g : Y ⟶ B), OpenEmbedding ⇑f → CompHausLike.HasExplicitPullback f g<GOAL>CompHausLike.HasExplicitPullbacksOfInclusions P
<VAR>P : TopCat → Prop<VAR>CompHausLike.HasExplicitFiniteCoproducts P<VAR>hP' : ∀ ⦃X Y B : CompHausLike P⦄ (f : X ⟶ B) (g : Y ⟶ B), OpenEmbedding ⇑f → CompHausLike.HasExplicitPullback f g<GOAL>CategoryTheory.FinitaryExtensive (CompHausLike P)
<VAR>B X : CompHaus<VAR>π : X ⟶ B<GOAL>[CategoryTheory.EffectiveEpi π, CategoryTheory.Epi π, Function.Surjective ⇑π].TFAE
<VAR>α : Type<VAR>Finite α<VAR>B : CompHaus<VAR>X : α → CompHaus<VAR>π : (a : α) → X a ⟶ B<GOAL>[CategoryTheory.EffectiveEpiFamily X π, CategoryTheory.Epi (CategoryTheory.Limits.Sigma.desc π), ∀ (b : ↑B.toTop), ∃ a x, (π a) x = b].TFAE
<VAR>α : Type<VAR>Finite α<VAR>B : CompHaus<VAR>X : α → CompHaus<VAR>π : (a : α) → X a ⟶ B<VAR>surj : ∀ (b : ↑B.toTop), ∃ a x, (π a) x = b<GOAL>CategoryTheory.EffectiveEpiFamily X π
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>self : CompletelyRegularSpace X<VAR>x : X<VAR>K : Set X<GOAL>IsClosed K → x ∉ K → ∃ f, Continuous f ∧ f x = 0 ∧ Set.EqOn f 1 K
<VAR>X : Type u<VAR>TopologicalSpace X<GOAL>CompletelyRegularSpace X ↔ ∀ (x : X) (K : Set X), IsClosed K → x ∉ K → ∃ f, Continuous f ∧ f x = 0 ∧ Set.EqOn f 1 K
<VAR>X : Type u<VAR>TopologicalSpace X<GOAL>T35Space X ↔ T1Space X ∧ CompletelyRegularSpace X
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>T1Space X<VAR>T35Space X<GOAL>Set.SeparatesPoints Continuous
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>T1Space X<VAR>T35Space X<GOAL>Function.Injective stoneCechUnit
<VAR>ι : Type v<VAR>α : ι → TopCat<VAR>X : CategoryTheory.Discrete ι<GOAL>(TopCat.piFan α).π.app X = TopCat.piπ α X.as
<VAR>ι : Type v<VAR>α : ι → TopCat<GOAL>(TopCat.piFan α).pt = TopCat.of ((i : ι) → ↑(α i))
<VAR>ι : Type v<VAR>α : ι → TopCat<VAR>i : ι<GOAL>(TopCat.piIsoPi α).inv ≫ CategoryTheory.Limits.Pi.π α i = TopCat.piπ α i
<VAR>ι : Type v<VAR>α : ι → TopCat<VAR>i : ι<VAR>x : (i : ι) → ↑(α i)<GOAL>(CategoryTheory.Limits.Pi.π α i) ((TopCat.piIsoPi α).inv x) = x i
<VAR>ι : Type v<VAR>α : ι → TopCat<VAR>i : ι<VAR>x : ↑(∏ᶜ α)<GOAL>(TopCat.piIsoPi α).hom x i = (CategoryTheory.Limits.Pi.π α i) x
<VAR>ι : Type v<VAR>α : ι → TopCat<VAR>X : CategoryTheory.Discrete ι<GOAL>(TopCat.sigmaCofan α).ι.app X = TopCat.sigmaι α X.as
<VAR>ι : Type v<VAR>α : ι → TopCat<GOAL>(TopCat.sigmaCofan α).pt = TopCat.of ((i : ι) × ↑(α i))
<VAR>ι : Type v<VAR>α : ι → TopCat<VAR>i : ι<GOAL>CategoryTheory.Limits.Sigma.ι α i ≫ (TopCat.sigmaIsoSigma α).hom = TopCat.sigmaι α i
<VAR>ι : Type v<VAR>α : ι → TopCat<VAR>i : ι<VAR>x : ↑(α i)<GOAL>(TopCat.sigmaIsoSigma α).hom ((CategoryTheory.Limits.Sigma.ι α i) x) = ⟨i, x⟩
<VAR>ι : Type v<VAR>α : ι → TopCat<VAR>i : ι<VAR>x : ↑(α i)<GOAL>(TopCat.sigmaIsoSigma α).inv ⟨i, x⟩ = (CategoryTheory.Limits.Sigma.ι α i) x
<VAR>J : Type v<VAR>CategoryTheory.SmallCategory J<VAR>F : J ⥤ TopCat<VAR>C : CategoryTheory.Limits.Cone F<VAR>hC : CategoryTheory.Limits.IsLimit C<GOAL>C.pt.str = ⨅ j, TopologicalSpace.induced (⇑(C.π.app j)) (F.obj j).str
<VAR>J : Type v<VAR>CategoryTheory.SmallCategory J<VAR>F : J ⥤ TopCat<GOAL>(CategoryTheory.Limits.limit F).str = ⨅ j, TopologicalSpace.induced (⇑(CategoryTheory.Limits.limit.π F j)) (F.obj j).str
<VAR>X Y : TopCat<GOAL>(X.prodIsoProd Y).hom ≫ TopCat.prodFst = CategoryTheory.Limits.prod.fst
<VAR>X Y : TopCat<GOAL>(X.prodIsoProd Y).hom ≫ TopCat.prodSnd = CategoryTheory.Limits.prod.snd
<VAR>X Y : TopCat<VAR>x : ↑(X ⨯ Y)<GOAL>(X.prodIsoProd Y).hom x = (CategoryTheory.Limits.prod.fst x, CategoryTheory.Limits.prod.snd x)
<VAR>X Y : TopCat<GOAL>(X.prodIsoProd Y).inv ≫ CategoryTheory.Limits.prod.fst = TopCat.prodFst
<VAR>X Y : TopCat<GOAL>(X.prodIsoProd Y).inv ≫ CategoryTheory.Limits.prod.snd = TopCat.prodSnd
<VAR>X Y : TopCat<GOAL>(X ⨯ Y).str = TopologicalSpace.induced (⇑CategoryTheory.Limits.prod.fst) X.str ⊓ TopologicalSpace.induced (⇑CategoryTheory.Limits.prod.snd) Y.str
<VAR>W X Y Z : TopCat<VAR>f : W ⟶ Y<VAR>g : X ⟶ Z<GOAL>Set.range ⇑(CategoryTheory.Limits.prod.map f g) = ⇑CategoryTheory.Limits.prod.fst ⁻¹' Set.range ⇑f ∩ ⇑CategoryTheory.Limits.prod.snd ⁻¹' Set.range ⇑g
<VAR>W X Y Z : TopCat<VAR>f : W ⟶ X<VAR>g : Y ⟶ Z<VAR>hf : Inducing ⇑f<VAR>hg : Inducing ⇑g<GOAL>Inducing ⇑(CategoryTheory.Limits.prod.map f g)
<VAR>W X Y Z : TopCat<VAR>f : W ⟶ X<VAR>g : Y ⟶ Z<VAR>hf : Embedding ⇑f<VAR>hg : Embedding ⇑g<GOAL>Embedding ⇑(CategoryTheory.Limits.prod.map f g)
<VAR>X Y : TopCat<VAR>c : CategoryTheory.Limits.BinaryCofan X Y<GOAL>Nonempty (CategoryTheory.Limits.IsColimit c) ↔ OpenEmbedding ⇑c.inl ∧ OpenEmbedding ⇑c.inr ∧ IsCompl (Set.range ⇑c.inl) (Set.range ⇑c.inr)
<VAR>X : Compactum<VAR>x : X.A<GOAL>X.str (X.incl x) = x
<VAR>X Y : Compactum<VAR>f : X ⟶ Y<VAR>xs : Ultrafilter X.A<GOAL>f.f (X.str xs) = Y.str (Ultrafilter.map f.f xs)
<VAR>X : Compactum<VAR>uux : Ultrafilter (Ultrafilter X.A)<GOAL>X.str (X.join uux) = X.str (Ultrafilter.map X.str uux)
<VAR>X : Compactum<VAR>A B : Set X.A<GOAL>Compactum.basic (A ∩ B) = Compactum.basic A ∩ Compactum.basic B
<VAR>X : Compactum<VAR>A : Set X.A<GOAL>A ⊆ Compactum.cl A
<VAR>X : Compactum<VAR>A : Set X.A<GOAL>Compactum.cl (Compactum.cl A) ⊆ Compactum.cl A
<VAR>X : Compactum<VAR>F : Ultrafilter X.A<VAR>x : X.A<GOAL>↑F ≤ 𝓝 x → X.str F = x
<VAR>X : Compactum<VAR>F : Ultrafilter X.A<VAR>x : X.A<GOAL>X.str F = x → ↑F ≤ 𝓝 x
<VAR>X : Compactum<VAR>A : Set X.A<GOAL>Compactum.cl A = closure A
<VAR>X : Type u_3<VAR>TopologicalSpace X<VAR>x : X<VAR>α : Type u_6<VAR>β : Type u_7<VAR>SMul α β<VAR>φ : (𝓝 x).Germ α<VAR>ψ : (𝓝 x).Germ β<GOAL>(φ • ψ).value = φ.value • ψ.value
<VAR>X : Type u_3<VAR>Y : Type u_4<VAR>TopologicalSpace X<VAR>f g : X → Y<VAR>A : Set X<VAR>P : (x : X) → (𝓝 x).Germ Y → Prop<VAR>hf : ∀ᶠ (x : X) in 𝓝ˢ A, P x ↑f<VAR>h : ∀ᶠ (z : X) in 𝓝ˢ A, g z = f z<GOAL>∀ᶠ (x : X) in 𝓝ˢ A, P x ↑g
<VAR>X : Type u_3<VAR>Y : Type u_4<VAR>TopologicalSpace X<VAR>f g : X → Y<VAR>A : Set X<VAR>x : X<VAR>P : (x : X) → (𝓝 x).Germ Y → Prop<VAR>hf : RestrictGermPredicate P A x ↑f<VAR>h : ∀ᶠ (z : X) in 𝓝ˢ A, g z = f z<GOAL>RestrictGermPredicate P A x ↑g
<VAR>X : Type u_3<VAR>Y : Type u_4<VAR>TopologicalSpace X<VAR>f : X → Y<VAR>A : Set X<VAR>P : (x : X) → (𝓝 x).Germ Y → Prop<GOAL>(∀ (x : X), RestrictGermPredicate P A x ↑f) ↔ ∀ᶠ (x : X) in 𝓝ˢ A, P x ↑f
<VAR>X : Type u_3<VAR>Y : Type u_4<VAR>TopologicalSpace X<VAR>f : X → Y<VAR>A : Set X<VAR>P : (x : X) → (𝓝 x).Germ Y → Prop<VAR>h : ∀ (x : X), P x ↑f<VAR>x : X<GOAL>RestrictGermPredicate P A x ↑f
<VAR>X : Type u_3<VAR>Y : Type u_4<VAR>Z : Type u_5<VAR>TopologicalSpace X<VAR>x : X<VAR>TopologicalSpace Y<VAR>y : Y<VAR>f : X × Y → Z<GOAL>(↑f).sliceLeft = ↑fun x' => f (x', y)
<VAR>X : Type u_3<VAR>Y : Type u_4<VAR>Z : Type u_5<VAR>TopologicalSpace X<VAR>x : X<VAR>TopologicalSpace Y<VAR>y : Y<VAR>f : X × Y → Z<GOAL>(↑f).sliceRight = ↑fun y' => f (x, y')
<VAR>X : Type u_3<VAR>Y : Type u_4<VAR>TopologicalSpace X<VAR>s : Set X<VAR>f : X → Y<VAR>x : ↑s<VAR>hf : (↑f).IsConstant<GOAL>(↑(f ∘ Subtype.val)).IsConstant
<VAR>X : Type u_3<VAR>Y : Type u_4<VAR>TopologicalSpace X<VAR>f : X → Y<VAR>h : ∀ (x : X), (↑f).IsConstant<GOAL>IsLocallyConstant f
<VAR>X : Type u_3<VAR>Y : Type u_4<VAR>TopologicalSpace X<VAR>f : X → Y<VAR>i : PreconnectedSpace X<VAR>h : ∀ (x : X), (↑f).IsConstant<VAR>x x' : X<GOAL>f x = f x'
<VAR>X : Type u_3<VAR>Y : Type u_4<VAR>TopologicalSpace X<VAR>f : X → Y<VAR>x : X<VAR>s : Set X<VAR>h : ∀ x ∈ s, (↑f).IsConstant<VAR>hs : IsPreconnected s<VAR>x' : X<VAR>x_in : x ∈ s<VAR>x'_in : x' ∈ s<GOAL>f x = f x'
<VAR>α : Type u_6<VAR>l : Filter α<VAR>R : Type u_7<VAR>AddCommMonoid R<VAR>ι : Type u_8<VAR>f : ι → α → R<VAR>s : Finset ι<GOAL>↑(∑ i ∈ s, f i) = ∑ i ∈ s, ↑(f i)
<VAR>α : Type u_6<VAR>l : Filter α<VAR>R : Type u_7<VAR>CommMonoid R<VAR>ι : Type u_8<VAR>f : ι → α → R<VAR>s : Finset ι<GOAL>↑(∏ i ∈ s, f i) = ∏ i ∈ s, ↑(f i)
<VAR>X Y B : CompHaus<VAR>f : X ⟶ B<VAR>g : Y ⟶ B<GOAL>CategoryTheory.CategoryStruct.comp (CompHaus.pullback.fst f g) f = CategoryTheory.CategoryStruct.comp (CompHaus.pullback.snd f g) g
<VAR>X Y B : CompHaus<VAR>f : X ⟶ B<VAR>g : Y ⟶ B<VAR>Z : CompHaus<VAR>a : Z ⟶ X<VAR>b : Z ⟶ Y<VAR>w : CategoryTheory.CategoryStruct.comp a f = CategoryTheory.CategoryStruct.comp b g<GOAL>CategoryTheory.CategoryStruct.comp (CompHaus.pullback.lift f g a b w) (CompHaus.pullback.fst f g) = a
<VAR>X Y B : CompHaus<VAR>f : X ⟶ B<VAR>g : Y ⟶ B<VAR>Z : CompHaus<VAR>a : Z ⟶ X<VAR>b : Z ⟶ Y<VAR>w : CategoryTheory.CategoryStruct.comp a f = CategoryTheory.CategoryStruct.comp b g<GOAL>CategoryTheory.CategoryStruct.comp (CompHaus.pullback.lift f g a b w) (CompHaus.pullback.snd f g) = b
<VAR>X Y B : CompHaus<VAR>f : X ⟶ B<VAR>g : Y ⟶ B<VAR>Z : CompHaus<VAR>a b : Z ⟶ CompHaus.pullback f g<VAR>hfst : CategoryTheory.CategoryStruct.comp a (CompHaus.pullback.fst f g) = CategoryTheory.CategoryStruct.comp b (CompHaus.pullback.fst f g)<VAR>hsnd : CategoryTheory.CategoryStruct.comp a (CompHaus.pullback.snd f g) = CategoryTheory.CategoryStruct.comp b (CompHaus.pullback.snd f g)<GOAL>a = b
<VAR>X Y B : CompHaus<VAR>f : X ⟶ B<VAR>g : Y ⟶ B<GOAL>(CompHaus.pullback.cone f g).π = { app := fun j => Option.rec (CategoryTheory.CategoryStruct.comp (CompHaus.pullback.fst f g) f) (fun val => CategoryTheory.Limits.WalkingPair.rec (CompHaus.pullback.fst f g) (CompHaus.pullback.snd f g) val) j, naturality := ⋯ }
<VAR>X Y B : CompHaus<VAR>f : X ⟶ B<VAR>g : Y ⟶ B<GOAL>(CompHaus.pullback.cone f g).pt = CompHaus.pullback f g
<VAR>X Y B : CompHaus<VAR>f : X ⟶ B<VAR>g : Y ⟶ B<VAR>s : CategoryTheory.Limits.PullbackCone f g<GOAL>(CompHaus.pullback.isLimit f g).lift s = CompHaus.pullback.lift f g s.fst s.snd ⋯
<VAR>X Y B : CompHaus<VAR>f : X ⟶ B<VAR>g : Y ⟶ B<GOAL>CompHaus.pullback.fst f g = CategoryTheory.CategoryStruct.comp (CompHaus.pullbackIsoPullback f g).hom (CategoryTheory.Limits.pullback.fst f g)
<VAR>X Y B : CompHaus<VAR>f : X ⟶ B<VAR>g : Y ⟶ B<GOAL>CompHaus.pullback.snd f g = CategoryTheory.CategoryStruct.comp (CompHaus.pullbackIsoPullback f g).hom (CategoryTheory.Limits.pullback.snd f g)
<VAR>α : Type w<VAR>Finite α<VAR>X : α → CompHaus<VAR>B : CompHaus<VAR>e : (a : α) → X a ⟶ B<VAR>a : α<GOAL>CategoryTheory.CategoryStruct.comp (CompHaus.finiteCoproduct.ι X a) (CompHaus.finiteCoproduct.desc X e) = e a
<VAR>α : Type w<VAR>Finite α<VAR>X : α → CompHaus<VAR>B : CompHaus<VAR>f g : CompHaus.finiteCoproduct X ⟶ B<VAR>h : ∀ (a : α), CategoryTheory.CategoryStruct.comp (CompHaus.finiteCoproduct.ι X a) f = CategoryTheory.CategoryStruct.comp (CompHaus.finiteCoproduct.ι X a) g<GOAL>f = g
<VAR>α : Type w<VAR>Finite α<VAR>X : α → CompHaus<VAR>a : α<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι X a) (CompHaus.coproductIsoCoproduct X).inv = CompHaus.finiteCoproduct.ι X a
<VAR>α : Type w<VAR>Finite α<VAR>X : α → CompHaus<VAR>a : α<GOAL>Function.Injective ⇑(CompHaus.finiteCoproduct.ι X a)
<VAR>α : Type w<VAR>Finite α<VAR>X : α → CompHaus<VAR>R : ↑(CompHaus.finiteCoproduct X).toTop<GOAL>∃ a r, R = (CompHaus.finiteCoproduct.ι X a) r
<VAR>α : Type w<VAR>Finite α<VAR>X : α → CompHaus<VAR>B : CompHaus<VAR>π : (a : α) → X a ⟶ B<VAR>a : α<VAR>x : (CategoryTheory.forget CompHaus).obj (X a)<GOAL>(CompHaus.finiteCoproduct.desc X π) ((CompHaus.finiteCoproduct.ι X a) x) = (π a) x