Loogle!

Result

Found 406 declarations mentioning CompHausLike.toTop. Of these, only the first 200 are shown.

• CompHausLike.toTop 📋 Mathlib.Topology.Category.CompHausLike.Basic
  {P : TopCat → Prop} (self : CompHausLike P) : TopCat
• CompHausLike.prop 📋 Mathlib.Topology.Category.CompHausLike.Basic
  {P : TopCat → Prop} (self : CompHausLike P) : P self.toTop
• CompHausLike.is_compact 📋 Mathlib.Topology.Category.CompHausLike.Basic
  {P : TopCat → Prop} (self : CompHausLike P) : CompactSpace ↑self.toTop
• CompHausLike.is_hausdorff 📋 Mathlib.Topology.Category.CompHausLike.Basic
  {P : TopCat → Prop} (self : CompHausLike P) : T2Space ↑self.toTop
• CompHausLike.instHasPropCarrierToTop 📋 Mathlib.Topology.Category.CompHausLike.Basic
  (P : TopCat → Prop) (X : CompHausLike P) : CompHausLike.HasProp P ↑X.toTop
• CompHausLike.const 📋 Mathlib.Topology.Category.CompHausLike.Basic
  {P : TopCat → Prop} (T : CompHausLike P) {S : CompHausLike P} (s : ↑S.toTop) : T ⟶ S
• CompHausLike.toCompHausLike 📋 Mathlib.Topology.Category.CompHausLike.Basic
  {P P' : TopCat → Prop} (h : ∀ (X : CompHausLike P), P X.toTop → P' X.toTop) : CategoryTheory.Functor (CompHausLike P) (CompHausLike P')
• CompHausLike.fullyFaithfulToCompHausLike 📋 Mathlib.Topology.Category.CompHausLike.Basic
  {P P' : TopCat → Prop} (h : ∀ (X : CompHausLike P), P X.toTop → P' X.toTop) : (CompHausLike.toCompHausLike h).FullyFaithful
• CompHausLike.instFaithfulToCompHausLike 📋 Mathlib.Topology.Category.CompHausLike.Basic
  {P P' : TopCat → Prop} (h : ∀ (X : CompHausLike P), P X.toTop → P' X.toTop) : (CompHausLike.toCompHausLike h).Faithful
• CompHausLike.instFullToCompHausLike 📋 Mathlib.Topology.Category.CompHausLike.Basic
  {P P' : TopCat → Prop} (h : ∀ (X : CompHausLike P), P X.toTop → P' X.toTop) : (CompHausLike.toCompHausLike h).Full
• CompHausLike.coe_of 📋 Mathlib.Topology.Category.CompHausLike.Basic
  (P : TopCat → Prop) (X : Type u) [TopologicalSpace X] [CompactSpace X] [T2Space X] [CompHausLike.HasProp P X] : ↑(CompHausLike.of P X).toTop = X
• CompHausLike.homeoOfIso 📋 Mathlib.Topology.Category.CompHausLike.Basic
  {P : TopCat → Prop} {X Y : CompHausLike P} (f : X ≅ Y) : ↑X.toTop ≃ₜ ↑Y.toTop
• CompHausLike.isoOfHomeo 📋 Mathlib.Topology.Category.CompHausLike.Basic
  {P : TopCat → Prop} {X Y : CompHausLike P} (f : ↑X.toTop ≃ₜ ↑Y.toTop) : X ≅ Y
• CompHausLike.isoEquivHomeo 📋 Mathlib.Topology.Category.CompHausLike.Basic
  {P : TopCat → Prop} {X Y : CompHausLike P} : (X ≅ Y) ≃ (↑X.toTop ≃ₜ ↑Y.toTop)
• CompHausLike.concreteCategory 📋 Mathlib.Topology.Category.CompHausLike.Basic
  (P : TopCat → Prop) : CategoryTheory.ConcreteCategory (CompHausLike P) fun x1 x2 => C(↑x1.toTop, ↑x2.toTop)
• CompHausLike.forget_reflectsIsomorphisms 📋 Mathlib.Topology.Category.CompHausLike.Basic
  {P : TopCat → Prop} : (CategoryTheory.forget (CompHausLike P)).ReflectsIsomorphisms
• CompHausLike.compHausLikeToTop_map 📋 Mathlib.Topology.Category.CompHausLike.Basic
  (P : TopCat → Prop) {X✝ Y✝ : CategoryTheory.InducedCategory TopCat CompHausLike.toTop} (f : X✝ ⟶ Y✝) : (CompHausLike.compHausLikeToTop P).map f = f.hom
• CompHausLike.hasForget₂ 📋 Mathlib.Topology.Category.CompHausLike.Basic
  (P : TopCat → Prop) : CategoryTheory.HasForget₂ (CompHausLike P) TopCat
• CompHausLike.coe_id 📋 Mathlib.Topology.Category.CompHausLike.Basic
  (P : TopCat → Prop) (X : CompHausLike P) : ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id X)) = id
• CompHausLike.hom_ofHom 📋 Mathlib.Topology.Category.CompHausLike.Basic
  (P : TopCat → Prop) {X : Type u} [TopologicalSpace X] [CompactSpace X] [T2Space X] [CompHausLike.HasProp P X] {Y : Type u} [TopologicalSpace Y] [CompactSpace Y] [T2Space Y] [CompHausLike.HasProp P Y] (f : C(X, Y)) : CategoryTheory.ConcreteCategory.hom (CompHausLike.ofHom P f) = f
• CompHausLike.isoOfBijective 📋 Mathlib.Topology.Category.CompHausLike.Basic
  {P : TopCat → Prop} {X Y : CompHausLike P} (f : X ⟶ Y) (bij : Function.Bijective ⇑(CategoryTheory.ConcreteCategory.hom f)) : X ≅ Y
• CompHausLike.epi_of_surjective 📋 Mathlib.Topology.Category.CompHausLike.Basic
  {P : TopCat → Prop} {X Y : CompHausLike P} (f : X ⟶ Y) (hf : Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f)) : CategoryTheory.Epi f
• CompHausLike.isClosedMap 📋 Mathlib.Topology.Category.CompHausLike.Basic
  {P : TopCat → Prop} {X Y : CompHausLike P} (f : X ⟶ Y) : IsClosedMap ⇑(CategoryTheory.ConcreteCategory.hom f)
• CompHausLike.isIso_of_bijective 📋 Mathlib.Topology.Category.CompHausLike.Basic
  {P : TopCat → Prop} {X Y : CompHausLike P} (f : X ⟶ Y) (bij : Function.Bijective ⇑(CategoryTheory.ConcreteCategory.hom f)) : CategoryTheory.IsIso f
• CompHausLike.mono_iff_injective 📋 Mathlib.Topology.Category.CompHausLike.Basic
  {P : TopCat → Prop} {X Y : CompHausLike P} (f : X ⟶ Y) : CategoryTheory.Mono f ↔ Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom f)
• CompHausLike.isoEquivHomeo_apply 📋 Mathlib.Topology.Category.CompHausLike.Basic
  {P : TopCat → Prop} {X Y : CompHausLike P} (f : X ≅ Y) : CompHausLike.isoEquivHomeo f = CompHausLike.homeoOfIso f
• CompHausLike.const_comp 📋 Mathlib.Topology.Category.CompHausLike.Basic
  {P : TopCat → Prop} {S T U : CompHausLike P} (s : ↑S.toTop) (g : S ⟶ U) : CategoryTheory.CategoryStruct.comp (T.const s) g = T.const ((CategoryTheory.ConcreteCategory.hom g) s)
• CompHausLike.homeoOfIso_apply 📋 Mathlib.Topology.Category.CompHausLike.Basic
  {P : TopCat → Prop} {X Y : CompHausLike P} (f : X ≅ Y) (a : ↑X.toTop) : (CompHausLike.homeoOfIso f) a = (CategoryTheory.ConcreteCategory.hom f.hom.hom) a
• CompHausLike.isoEquivHomeo_symm_apply 📋 Mathlib.Topology.Category.CompHausLike.Basic
  {P : TopCat → Prop} {X Y : CompHausLike P} (f : ↑X.toTop ≃ₜ ↑Y.toTop) : CompHausLike.isoEquivHomeo.symm f = CompHausLike.isoOfHomeo f
• CompHausLike.toCompHausLike_map 📋 Mathlib.Topology.Category.CompHausLike.Basic
  {P P' : TopCat → Prop} (h : ∀ (X : CompHausLike P), P X.toTop → P' X.toTop) {X Y : CompHausLike P} (f : X ⟶ Y) : (CompHausLike.toCompHausLike h).map f = CategoryTheory.ConcreteCategory.ofHom (TopCat.Hom.hom f.hom)
• CompHausLike.homeoOfIso_symm_apply 📋 Mathlib.Topology.Category.CompHausLike.Basic
  {P : TopCat → Prop} {X Y : CompHausLike P} (f : X ≅ Y) (a : ↑Y.toTop) : (CompHausLike.homeoOfIso f).symm a = (CategoryTheory.ConcreteCategory.hom f.inv.hom) a
• CompHausLike.isoOfHomeo_hom_hom_hom_apply 📋 Mathlib.Topology.Category.CompHausLike.Basic
  {P : TopCat → Prop} {X Y : CompHausLike P} (f : ↑X.toTop ≃ₜ ↑Y.toTop) (a : ↑((CompHausLike.compHausLikeToTop P).obj X)) : (TopCat.Hom.hom (CompHausLike.isoOfHomeo f).hom.hom) a = f a
• CompHausLike.coe_comp 📋 Mathlib.Topology.Category.CompHausLike.Basic
  (P : TopCat → Prop) {X Y Z : CompHausLike P} (f : X ⟶ Y) (g : Y ⟶ Z) : ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) = ⇑(CategoryTheory.ConcreteCategory.hom g) ∘ ⇑(CategoryTheory.ConcreteCategory.hom f)
• CompHausLike.isoOfHomeo_inv_hom_hom_apply 📋 Mathlib.Topology.Category.CompHausLike.Basic
  {P : TopCat → Prop} {X Y : CompHausLike P} (f : ↑X.toTop ≃ₜ ↑Y.toTop) (a : ↑((CompHausLike.compHausLikeToTop P).obj Y)) : (TopCat.Hom.hom (CompHausLike.isoOfHomeo f).inv.hom) a = f.symm a
• CompHaus.instCompactSpaceCarrierToTopTrue 📋 Mathlib.Topology.Category.CompHaus.Basic
  {X : CompHaus} : CompactSpace ↑X.toTop
• CompHaus.instT2SpaceCarrierToTopTrue 📋 Mathlib.Topology.Category.CompHaus.Basic
  {X : CompHaus} : T2Space ↑X.toTop
• stoneCechObj_toTop_carrier 📋 Mathlib.Topology.Category.CompHaus.Basic
  (X : TopCat) : ↑(stoneCechObj X).toTop = StoneCech ↑X
• topToCompHaus_obj 📋 Mathlib.Topology.Category.CompHaus.Basic
  (X : TopCat) : ↑(topToCompHaus.obj X).toTop = StoneCech ↑X
• CompHaus.epi_iff_surjective 📋 Mathlib.Topology.Category.CompHaus.Basic
  {X Y : CompHaus} (f : X ⟶ Y) : CategoryTheory.Epi f ↔ Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f)
• uCompactlyGeneratedSpace_of_isClosed 📋 Mathlib.Topology.Compactness.CompactlyGeneratedSpace
  {X : Type w} [tX : TopologicalSpace X] (h : ∀ (s : Set X), (∀ (S : CompHaus) (f : C(↑S.toTop, X)), IsClosed (⇑f ⁻¹' s)) → IsClosed s) : UCompactlyGeneratedSpace X
• uCompactlyGeneratedSpace_of_isOpen 📋 Mathlib.Topology.Compactness.CompactlyGeneratedSpace
  {X : Type w} [tX : TopologicalSpace X] (h : ∀ (s : Set X), (∀ (S : CompHaus) (f : C(↑S.toTop, X)), IsOpen (⇑f ⁻¹' s)) → IsOpen s) : UCompactlyGeneratedSpace X
• UCompactlyGeneratedSpace.isClosed 📋 Mathlib.Topology.Compactness.CompactlyGeneratedSpace
  {X : Type w} [tX : TopologicalSpace X] [UCompactlyGeneratedSpace X] {s : Set X} (hs : ∀ (S : CompHaus) (f : C(↑S.toTop, X)), IsClosed (⇑f ⁻¹' s)) : IsClosed s
• UCompactlyGeneratedSpace.isOpen 📋 Mathlib.Topology.Compactness.CompactlyGeneratedSpace
  {X : Type w} [tX : TopologicalSpace X] [UCompactlyGeneratedSpace X] {s : Set X} (hs : ∀ (S : CompHaus) (f : C(↑S.toTop, X)), IsOpen (⇑f ⁻¹' s)) : IsOpen s
• continuous_from_compactlyGenerated 📋 Mathlib.Topology.Compactness.CompactlyGeneratedSpace
  {X : Type w} {Y : Type x} [TopologicalSpace X] [t : TopologicalSpace Y] (f : X → Y) (h : ∀ (S : CompHaus) (g : C(↑S.toTop, X)), Continuous (f ∘ ⇑g)) : Continuous f
• continuous_from_uCompactlyGeneratedSpace 📋 Mathlib.Topology.Compactness.CompactlyGeneratedSpace
  {X : Type w} {Y : Type x} [tX : TopologicalSpace X] [tY : TopologicalSpace Y] [UCompactlyGeneratedSpace X] (f : X → Y) (h : ∀ (S : CompHaus) (g : C(↑S.toTop, X)), Continuous (f ∘ ⇑g)) : Continuous f
• uCompactlyGeneratedSpace_of_continuous_maps 📋 Mathlib.Topology.Compactness.CompactlyGeneratedSpace
  {X : Type w} [t : TopologicalSpace X] (h : ∀ {Y : Type w} [tY : TopologicalSpace Y] (f : X → Y), (∀ (S : CompHaus) (g : C(↑S.toTop, X)), Continuous (f ∘ ⇑g)) → Continuous f) : UCompactlyGeneratedSpace X
• CompHausLike.instPreservesFiniteCoproductsToCompHausLike 📋 Mathlib.Topology.Category.CompHausLike.Limits
  {P : TopCat → Prop} [CompHausLike.HasExplicitFiniteCoproducts P] {P' : TopCat → Prop} (h : ∀ (X : CompHausLike P), P X.toTop → P' X.toTop) : CategoryTheory.Limits.PreservesFiniteCoproducts (CompHausLike.toCompHausLike h)
• CompHausLike.instPreservesLimitWalkingCospanCospanToCompHausLike 📋 Mathlib.Topology.Category.CompHausLike.Limits
  {P : TopCat → Prop} {X Y B : CompHausLike P} (f : X ⟶ B) (g : Y ⟶ B) [CompHausLike.HasExplicitPullback f g] {P' : TopCat → Prop} (h : ∀ (X : CompHausLike P), P X.toTop → P' X.toTop) : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f g) (CompHausLike.toCompHausLike h)
• CompHausLike.finiteCoproduct.ι_injective 📋 Mathlib.Topology.Category.CompHausLike.Limits
  {P : TopCat → Prop} {α : Type w} [Finite α] (X : α → CompHausLike P) [CompHausLike.HasExplicitFiniteCoproduct X] (a : α) : Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom (CompHausLike.finiteCoproduct.ι X a))
• CompHausLike.hasPullbacksOfInclusions 📋 Mathlib.Topology.Category.CompHausLike.Limits
  {P : TopCat → Prop} [CompHausLike.HasExplicitFiniteCoproducts P] (hP' : ∀ ⦃X Y B : CompHausLike P⦄ (f : X ⟶ B) (g : Y ⟶ B), Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f) → CompHausLike.HasExplicitPullback f g) : CompHausLike.HasExplicitPullbacksOfInclusions P
• CompHausLike.finitaryExtensive 📋 Mathlib.Topology.Category.CompHausLike.Limits
  {P : TopCat → Prop} [CompHausLike.HasExplicitFiniteCoproducts P] (hP' : ∀ ⦃X Y B : CompHausLike P⦄ (f : X ⟶ B) (g : Y ⟶ B), Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f) → CompHausLike.HasExplicitPullback f g) : CategoryTheory.FinitaryExtensive (CompHausLike P)
• CompHausLike.finiteCoproduct.ι_jointly_surjective 📋 Mathlib.Topology.Category.CompHausLike.Limits
  {P : TopCat → Prop} {α : Type w} [Finite α] (X : α → CompHausLike P) [CompHausLike.HasExplicitFiniteCoproduct X] (R : ↑(CompHausLike.finiteCoproduct X).toTop) : ∃ a r, R = (CategoryTheory.ConcreteCategory.hom (CompHausLike.finiteCoproduct.ι X a)) r
• CompHausLike.finiteCoproduct.isOpenEmbedding_ι 📋 Mathlib.Topology.Category.CompHausLike.Limits
  {P : TopCat → Prop} {α : Type w} [Finite α] (X : α → CompHausLike P) [CompHausLike.HasExplicitFiniteCoproduct X] (a : α) : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom (CompHausLike.finiteCoproduct.ι X a))
• CompHausLike.Sigma.isOpenEmbedding_ι 📋 Mathlib.Topology.Category.CompHausLike.Limits
  {P : TopCat → Prop} {α : Type w} [Finite α] (X : α → CompHausLike P) [CompHausLike.HasExplicitFiniteCoproduct X] (a : α) : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Sigma.ι X a))
• CompHausLike.finiteCoproduct.ι_desc_apply 📋 Mathlib.Topology.Category.CompHausLike.Limits
  {P : TopCat → Prop} {α : Type w} [Finite α] (X : α → CompHausLike P) [CompHausLike.HasExplicitFiniteCoproduct X] {B : CompHausLike P} {π : (a : α) → X a ⟶ B} (a : α) (x : (fun X => ↑X.toTop) (X a)) : (CategoryTheory.ConcreteCategory.hom (CompHausLike.finiteCoproduct.desc X π)) ((CategoryTheory.ConcreteCategory.hom (CompHausLike.finiteCoproduct.ι X a)) x) = (CategoryTheory.ConcreteCategory.hom (π a)) x
• CompHausLike.effectiveEpiStruct 📋 Mathlib.Topology.Category.CompHausLike.EffectiveEpi
  {P : TopCat → Prop} {B X : CompHausLike P} (π : X ⟶ B) (hπ : Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom π)) : CategoryTheory.EffectiveEpiStruct π
• CompHausLike.preregular 📋 Mathlib.Topology.Category.CompHausLike.EffectiveEpi
  {P : TopCat → Prop} [CompHausLike.HasExplicitPullbacks P] (hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), CategoryTheory.EffectiveEpi f → Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f)) : CategoryTheory.Preregular (CompHausLike P)
• CompHausLike.precoherent 📋 Mathlib.Topology.Category.CompHausLike.EffectiveEpi
  {P : TopCat → Prop} [CompHausLike.HasExplicitPullbacks P] [CompHausLike.HasExplicitFiniteCoproducts P] (hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), CategoryTheory.EffectiveEpi f → Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f)) : CategoryTheory.Precoherent (CompHausLike P)
• CompHaus.effectiveEpi_tfae 📋 Mathlib.Topology.Category.CompHaus.EffectiveEpi
  {B X : CompHaus} (π : X ⟶ B) : [CategoryTheory.EffectiveEpi π, CategoryTheory.Epi π, Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom π)].TFAE
• CompHaus.effectiveEpiFamily_of_jointly_surjective 📋 Mathlib.Topology.Category.CompHaus.EffectiveEpi
  {α : Type} [Finite α] {B : CompHaus} (X : α → CompHaus) (π : (a : α) → X a ⟶ B) (surj : ∀ (b : ↑B.toTop), ∃ a x, (CategoryTheory.ConcreteCategory.hom (π a)) x = b) : CategoryTheory.EffectiveEpiFamily X π
• CompHaus.effectiveEpiFamily_tfae 📋 Mathlib.Topology.Category.CompHaus.EffectiveEpi
  {α : Type} [Finite α] {B : CompHaus} (X : α → CompHaus) (π : (a : α) → X a ⟶ B) : [CategoryTheory.EffectiveEpiFamily X π, CategoryTheory.Epi (CategoryTheory.Limits.Sigma.desc π), ∀ (b : ↑B.toTop), ∃ a x, (CategoryTheory.ConcreteCategory.hom (π a)) x = b].TFAE
• Profinite.instTotallyDisconnectedSpaceCarrierToTop 📋 Mathlib.Topology.Category.Profinite.Basic
  {X : Profinite} : TotallyDisconnectedSpace ↑X.toTop
• instFiniteCarrierToTopTotallyDisconnectedSpaceObjFintypeCatProfiniteToProfinite 📋 Mathlib.Topology.Category.Profinite.Basic
  (X : FintypeCat) : Finite ↑(FintypeCat.toProfinite.obj X).toTop
• CompHaus.toProfinite_obj' 📋 Mathlib.Topology.Category.Profinite.Basic
  (X : CompHaus) : ↑(CompHaus.toProfinite.obj X).toTop = ConnectedComponents ↑X.toTop
• instTotallyDisconnectedSpaceCarrierToTopTrueObjProfiniteCompHausProfiniteToCompHaus 📋 Mathlib.Topology.Category.Profinite.Basic
  {X : Profinite} : TotallyDisconnectedSpace ↑(profiniteToCompHaus.obj X).toTop
• instFiniteCarrierToTopTotallyDisconnectedSpaceOfObj 📋 Mathlib.Topology.Category.Profinite.Basic
  (X : FintypeCat) : Finite ↑(Profinite.of X.obj).toTop
• Profinite.forget_preservesLimits 📋 Mathlib.Topology.Category.Profinite.Basic
  : CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget Profinite)
• FintypeCat.toProfinite_map_hom_hom_apply 📋 Mathlib.Topology.Category.Profinite.Basic
  {X✝ Y✝ : FintypeCat} (f : X✝ ⟶ Y✝) (a : X✝.obj) : (TopCat.Hom.hom (FintypeCat.toProfinite.map f).hom) a = (CategoryTheory.ConcreteCategory.hom f) a
• Profinite.epi_iff_surjective 📋 Mathlib.Topology.Category.Profinite.Basic
  {X Y : Profinite} (f : X ⟶ Y) : CategoryTheory.Epi f ↔ Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f)
• CompHaus.instExtremallyDisconnectedCarrierToTopTrueOfProjective 📋 Mathlib.Topology.Category.Stonean.Basic
  (X : CompHaus) [CategoryTheory.Projective X] : ExtremallyDisconnected ↑X.toTop
• CompHaus.Gleason 📋 Mathlib.Topology.Category.Stonean.Basic
  (X : CompHaus) : CategoryTheory.Projective X ↔ ExtremallyDisconnected ↑X.toTop
• Stonean.instExtremallyDisconnectedCarrierToTop 📋 Mathlib.Topology.Category.Stonean.Basic
  (X : Stonean) : ExtremallyDisconnected ↑X.toTop
• CompHaus.toStonean_toTop 📋 Mathlib.Topology.Category.Stonean.Basic
  (X : CompHaus) [CategoryTheory.Projective X] : X.toStonean.toTop = X.toTop
• Profinite.projective_of_extrDisc 📋 Mathlib.Topology.Category.Stonean.Basic
  {X : Profinite} (hX : ExtremallyDisconnected ↑X.toTop) : CategoryTheory.Projective X
• Stonean.epi_iff_surjective 📋 Mathlib.Topology.Category.Stonean.Basic
  {X Y : Stonean} (f : X ⟶ Y) : CategoryTheory.Epi f ↔ Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f)
• Profinite.effectiveEpi_tfae 📋 Mathlib.Topology.Category.Profinite.EffectiveEpi
  {B X : Profinite} (π : X ⟶ B) : [CategoryTheory.EffectiveEpi π, CategoryTheory.Epi π, Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom π)].TFAE
• Profinite.effectiveEpiFamily_of_jointly_surjective 📋 Mathlib.Topology.Category.Profinite.EffectiveEpi
  {α : Type} [Finite α] {B : Profinite} (X : α → Profinite) (π : (a : α) → X a ⟶ B) (surj : ∀ (b : ↑B.toTop), ∃ a x, (CategoryTheory.ConcreteCategory.hom (π a)) x = b) : CategoryTheory.EffectiveEpiFamily X π
• Profinite.effectiveEpiFamily_tfae 📋 Mathlib.Topology.Category.Profinite.EffectiveEpi
  {α : Type} [Finite α] {B : Profinite} (X : α → Profinite) (π : (a : α) → X a ⟶ B) : [CategoryTheory.EffectiveEpiFamily X π, CategoryTheory.Epi (CategoryTheory.Limits.Sigma.desc π), ∀ (b : ↑B.toTop), ∃ a x, (CategoryTheory.ConcreteCategory.hom (π a)) x = b].TFAE
• Stonean.extremallyDisconnected_preimage 📋 Mathlib.Topology.Category.Stonean.Limits
  {X Y Z : Stonean} {f : X ⟶ Z} (i : Y ⟶ Z) (hi : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) : ExtremallyDisconnected ↑(⇑(CategoryTheory.ConcreteCategory.hom i) ⁻¹' Set.range ⇑(CategoryTheory.ConcreteCategory.hom f))
• Stonean.extremallyDisconnected_pullback 📋 Mathlib.Topology.Category.Stonean.Limits
  {X Y Z : Stonean} {f : X ⟶ Z} (i : Y ⟶ Z) (hi : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) : ExtremallyDisconnected ↑{xy | (CategoryTheory.ConcreteCategory.hom f) xy.1 = (CategoryTheory.ConcreteCategory.hom i) xy.2}
• Stonean.effectiveEpi_tfae 📋 Mathlib.Topology.Category.Stonean.EffectiveEpi
  {B X : Stonean} (π : X ⟶ B) : [CategoryTheory.EffectiveEpi π, CategoryTheory.Epi π, Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom π)].TFAE
• Stonean.effectiveEpiFamily_of_jointly_surjective 📋 Mathlib.Topology.Category.Stonean.EffectiveEpi
  {α : Type} [Finite α] {B : Stonean} (X : α → Stonean) (π : (a : α) → X a ⟶ B) (surj : ∀ (b : ↑B.toTop), ∃ a x, (CategoryTheory.ConcreteCategory.hom (π a)) x = b) : CategoryTheory.EffectiveEpiFamily X π
• Stonean.effectiveEpiFamily_tfae 📋 Mathlib.Topology.Category.Stonean.EffectiveEpi
  {α : Type} [Finite α] {B : Stonean} (X : α → Stonean) (π : (a : α) → X a ⟶ B) : [CategoryTheory.EffectiveEpiFamily X π, CategoryTheory.Epi (CategoryTheory.Limits.Sigma.desc π), ∀ (b : ↑B.toTop), ∃ a x, (CategoryTheory.ConcreteCategory.hom (π a)) x = b].TFAE
• Profinite.fintypeDiagram 📋 Mathlib.Topology.Category.Profinite.AsLimit
  (X : Profinite) : CategoryTheory.Functor (DiscreteQuotient ↑X.toTop) FintypeCat
• Profinite.diagram 📋 Mathlib.Topology.Category.Profinite.AsLimit
  (X : Profinite) : CategoryTheory.Functor (DiscreteQuotient ↑X.toTop) Profinite
• Profinite.asLimitCone 📋 Mathlib.Topology.Category.Profinite.AsLimit
  (X : Profinite) : CategoryTheory.Limits.Cone X.diagram
• Profinite.lim 📋 Mathlib.Topology.Category.Profinite.AsLimit
  (X : Profinite) : CategoryTheory.Limits.LimitCone X.diagram
• Profinite.asLimit 📋 Mathlib.Topology.Category.Profinite.AsLimit
  (X : Profinite) : CategoryTheory.Limits.IsLimit X.asLimitCone
• Profinite.isoAsLimitConeLift 📋 Mathlib.Topology.Category.Profinite.AsLimit
  (X : Profinite) : X ≅ (Profinite.limitCone X.diagram).pt
• Profinite.asLimitConeIso 📋 Mathlib.Topology.Category.Profinite.AsLimit
  (X : Profinite) : X.asLimitCone ≅ Profinite.limitCone X.diagram
• Profinite.isIso_asLimitCone_lift 📋 Mathlib.Topology.Category.Profinite.AsLimit
  (X : Profinite) : CategoryTheory.IsIso ((Profinite.limitConeIsLimit X.diagram).lift X.asLimitCone)
• Profinite.exists_locallyConstant 📋 Mathlib.Topology.Category.Profinite.CofilteredLimit
  {J : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.IsCofiltered J] {F : CategoryTheory.Functor J Profinite} (C : CategoryTheory.Limits.Cone F) {α : Type u_1} (hC : CategoryTheory.Limits.IsLimit C) (f : LocallyConstant (↑C.pt.toTop) α) : ∃ j g, f = LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom) g
• Profinite.exists_locallyConstant_finite_nonempty 📋 Mathlib.Topology.Category.Profinite.CofilteredLimit
  {J : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.IsCofiltered J] {F : CategoryTheory.Functor J Profinite} (C : CategoryTheory.Limits.Cone F) {α : Type u_1} [Finite α] [Nonempty α] (hC : CategoryTheory.Limits.IsLimit C) (f : LocallyConstant (↑C.pt.toTop) α) : ∃ j g, f = LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom) g
• Profinite.exists_locallyConstant_fin_two 📋 Mathlib.Topology.Category.Profinite.CofilteredLimit
  {J : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.IsCofiltered J] {F : CategoryTheory.Functor J Profinite} (C : CategoryTheory.Limits.Cone F) (hC : CategoryTheory.Limits.IsLimit C) (f : LocallyConstant (↑C.pt.toTop) (Fin 2)) : ∃ j g, f = LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom) g
• Profinite.exists_locallyConstant_finite_aux 📋 Mathlib.Topology.Category.Profinite.CofilteredLimit
  {J : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.IsCofiltered J] {F : CategoryTheory.Functor J Profinite} (C : CategoryTheory.Limits.Cone F) {α : Type u_1} [Finite α] (hC : CategoryTheory.Limits.IsLimit C) (f : LocallyConstant (↑C.pt.toTop) α) : ∃ j g, LocallyConstant.map (fun a b => if a = b then 0 else 1) f = LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom) g
• Profinite.exists_isClopen_of_cofiltered 📋 Mathlib.Topology.Category.Profinite.CofilteredLimit
  {J : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.IsCofiltered J] {F : CategoryTheory.Functor J Profinite} (C : CategoryTheory.Limits.Cone F) {U : Set ↑C.pt.toTop} (hC : CategoryTheory.Limits.IsLimit C) (hU : IsClopen U) : ∃ j V, IsClopen V ∧ U = ⇑(CategoryTheory.ConcreteCategory.hom (C.π.app j)) ⁻¹' V
• LightProfinite.instSecondCountableTopologyCarrierToTopAndTotallyDisconnectedSpace 📋 Mathlib.Topology.Category.LightProfinite.Basic
  {X : LightProfinite} : SecondCountableTopology ↑X.toTop
• LightProfinite.instTotallyDisconnectedSpaceCarrierToTopAndSecondCountableTopology 📋 Mathlib.Topology.Category.LightProfinite.Basic
  {X : LightProfinite} : TotallyDisconnectedSpace ↑X.toTop
• LightProfinite.instCountableClopensCarrierToTopAndTotallyDisconnectedSpaceSecondCountableTopology 📋 Mathlib.Topology.Category.LightProfinite.Basic
  (S : LightProfinite) : Countable (TopologicalSpace.Clopens ↑S.toTop)
• instFiniteCarrierToTopAndTotallyDisconnectedSpaceSecondCountableTopologyObjFintypeCatLightProfiniteToLightProfinite 📋 Mathlib.Topology.Category.LightProfinite.Basic
  (X : FintypeCat) : Finite ↑(FintypeCat.toLightProfinite.obj X).toTop
• LightProfinite.instCountableDiscreteQuotient 📋 Mathlib.Topology.Category.LightProfinite.Basic
  (S : LightProfinite) : Countable (DiscreteQuotient ↑(lightToProfinite.obj S).toTop)
• LightDiagram.hasForget 📋 Mathlib.Topology.Category.LightProfinite.Basic
  : CategoryTheory.ConcreteCategory LightDiagram fun X Y => C(↑X.toProfinite.toTop, ↑Y.toProfinite.toTop)
• instSecondCountableTopologyCarrierToTopTotallyDisconnectedSpacePtOppositeNatProfiniteCone 📋 Mathlib.Topology.Category.LightProfinite.Basic
  (S : LightDiagram) : SecondCountableTopology ↑S.cone.pt.toTop
• instFiniteCarrierToTopAndTotallyDisconnectedSpaceSecondCountableTopologyOfObj 📋 Mathlib.Topology.Category.LightProfinite.Basic
  (X : FintypeCat) : Finite ↑(LightProfinite.of X.obj).toTop
• lightDiagramToLightProfinite_obj 📋 Mathlib.Topology.Category.LightProfinite.Basic
  (X : LightDiagram) : lightDiagramToLightProfinite.obj X = LightProfinite.of ↑X.cone.pt.toTop
• LightProfinite.instTotallyDisconnectedSpaceCarrierToTopTruePtCompHausLimitConeCompLightProfiniteToCompHaus 📋 Mathlib.Topology.Category.LightProfinite.Basic
  {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J LightProfinite) : TotallyDisconnectedSpace ↑(CompHaus.limitCone (F.comp lightProfiniteToCompHaus)).pt.toTop
• lightProfiniteToLightDiagram_map 📋 Mathlib.Topology.Category.LightProfinite.Basic
  {X✝ Y✝ : LightProfinite} (f : X✝ ⟶ Y✝) : lightProfiniteToLightDiagram.map f = CategoryTheory.InducedCategory.homMk (CategoryTheory.InducedCategory.homMk f.hom)
• LightDiagram.id_hom_hom_hom_apply 📋 Mathlib.Topology.Category.LightProfinite.Basic
  (X : LightDiagram) (a : ↑X.toProfinite.toTop) : (TopCat.Hom.hom (CategoryTheory.CategoryStruct.id X).hom.hom) a = a
• LightProfinite.forget_reflectsIsomorphisms 📋 Mathlib.Topology.Category.LightProfinite.Basic
  : (CategoryTheory.forget LightProfinite).ReflectsIsomorphisms
• LightProfinite.instPreservesLimitsOfShapeOppositeNatForgetContinuousMapCarrierToTopAndTotallyDisconnectedSpaceSecondCountableTopology 📋 Mathlib.Topology.Category.LightProfinite.Basic
  : CategoryTheory.Limits.PreservesLimitsOfShape ℕᵒᵖ (CategoryTheory.forget LightProfinite)
• FintypeCat.toLightProfinite_map_hom_hom_apply 📋 Mathlib.Topology.Category.LightProfinite.Basic
  {X✝ Y✝ : FintypeCat} (f : X✝ ⟶ Y✝) (a : X✝.obj) : (TopCat.Hom.hom (FintypeCat.toLightProfinite.map f).hom) a = (CategoryTheory.ConcreteCategory.hom f) a
• LightDiagram.comp_hom_hom_hom_apply 📋 Mathlib.Topology.Category.LightProfinite.Basic
  {X Y Z : LightDiagram} (a✝ : X ⟶ Y) (a✝¹ : Y ⟶ Z) (a✝² : ↑X.toProfinite.toTop) : (TopCat.Hom.hom (CategoryTheory.CategoryStruct.comp a✝ a✝¹).hom.hom) a✝² = a✝¹.hom.hom.hom' (a✝.hom.hom.hom' a✝²)
• LightProfinite.isoOfBijective 📋 Mathlib.Topology.Category.LightProfinite.Basic
  {X Y : LightProfinite} (f : X ⟶ Y) (bij : Function.Bijective ⇑(CategoryTheory.ConcreteCategory.hom f)) : X ≅ Y
• LightProfinite.isIso_of_bijective 📋 Mathlib.Topology.Category.LightProfinite.Basic
  {X Y : LightProfinite} (f : X ⟶ Y) (bij : Function.Bijective ⇑(CategoryTheory.ConcreteCategory.hom f)) : CategoryTheory.IsIso f
• LightProfinite.epi_iff_surjective 📋 Mathlib.Topology.Category.LightProfinite.Basic
  {X Y : LightProfinite} (f : X ⟶ Y) : CategoryTheory.Epi f ↔ Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f)
• LightProfinite.isClosedMap 📋 Mathlib.Topology.Category.LightProfinite.Basic
  {X Y : LightProfinite} (f : X ⟶ Y) : IsClosedMap ⇑(CategoryTheory.ConcreteCategory.hom f)
• lightDiagramToLightProfinite_map 📋 Mathlib.Topology.Category.LightProfinite.Basic
  {X✝ Y✝ : LightDiagram} (f : X✝ ⟶ Y✝) : lightDiagramToLightProfinite.map f = CategoryTheory.InducedCategory.homMk f.hom.hom
• LightProfinite.instEpiCompHausLikeAndTotallyDisconnectedSpaceCarrierSecondCountableTopologyFst 📋 Mathlib.Topology.Category.LightProfinite.Limits
  {X Y Z : LightProfinite} (f : X ⟶ Z) (g : Y ⟶ Z) [h : CategoryTheory.Epi g] : CategoryTheory.Epi (CompHausLike.pullback.fst f g)
• LightProfinite.instEpiCompHausLikeAndTotallyDisconnectedSpaceCarrierSecondCountableTopologySnd 📋 Mathlib.Topology.Category.LightProfinite.Limits
  {X Y Z : LightProfinite} (f : X ⟶ Z) (g : Y ⟶ Z) [h : CategoryTheory.Epi f] : CategoryTheory.Epi (CompHausLike.pullback.snd f g)
• LightProfinite.effectiveEpi_iff_surjective 📋 Mathlib.Topology.Category.LightProfinite.EffectiveEpi
  {X Y : LightProfinite} (f : X ⟶ Y) : CategoryTheory.EffectiveEpi f ↔ Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f)
• TopCat.toSheafCompHausLike 📋 Mathlib.Condensed.TopComparison
  (P : TopCat → Prop) (X : TopCat) [CompHausLike.HasExplicitFiniteCoproducts P] [CompHausLike.HasExplicitPullbacks P] (hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), CategoryTheory.EffectiveEpi f → Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f)) : have this := ⋯; CategoryTheory.Sheaf (CategoryTheory.coherentTopology (CompHausLike P)) (Type (max u w))
• topCatToSheafCompHausLike 📋 Mathlib.Condensed.TopComparison
  (P : TopCat → Prop) [CompHausLike.HasExplicitFiniteCoproducts P] [CompHausLike.HasExplicitPullbacks P] (hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), CategoryTheory.EffectiveEpi f → Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f)) : have this := ⋯; CategoryTheory.Functor TopCat (CategoryTheory.Sheaf (CategoryTheory.coherentTopology (CompHausLike P)) (Type (max u w)))
• TopCat.toSheafCompHausLike_obj_obj 📋 Mathlib.Condensed.TopComparison
  (P : TopCat → Prop) (X : TopCat) [CompHausLike.HasExplicitFiniteCoproducts P] [CompHausLike.HasExplicitPullbacks P] (hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), CategoryTheory.EffectiveEpi f → Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f)) (X✝ : (CompHausLike P)ᵒᵖ) : (TopCat.toSheafCompHausLike P X hs).obj.obj X✝ = C(↑((CompHausLike.compHausLikeToTop P).obj (Opposite.unop X✝)), ↑X)
• topCatToSheafCompHausLike_obj 📋 Mathlib.Condensed.TopComparison
  (P : TopCat → Prop) [CompHausLike.HasExplicitFiniteCoproducts P] [CompHausLike.HasExplicitPullbacks P] (hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), CategoryTheory.EffectiveEpi f → Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f)) (X : TopCat) : (topCatToSheafCompHausLike P hs).obj X = TopCat.toSheafCompHausLike P X hs
• TopCat.toSheafCompHausLike_obj_map 📋 Mathlib.Condensed.TopComparison
  (P : TopCat → Prop) (X : TopCat) [CompHausLike.HasExplicitFiniteCoproducts P] [CompHausLike.HasExplicitPullbacks P] (hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), CategoryTheory.EffectiveEpi f → Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f)) {X✝ Y✝ : (CompHausLike P)ᵒᵖ} (f : X✝ ⟶ Y✝) : (TopCat.toSheafCompHausLike P X hs).obj.map f = TypeCat.ofHom fun g => g.comp (TopCat.Hom.hom f.unop.hom)
• topCatToSheafCompHausLike_map_hom_app 📋 Mathlib.Condensed.TopComparison
  (P : TopCat → Prop) [CompHausLike.HasExplicitFiniteCoproducts P] [CompHausLike.HasExplicitPullbacks P] (hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), CategoryTheory.EffectiveEpi f → Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f)) {X✝ Y✝ : TopCat} (f : X✝ ⟶ Y✝) (x✝ : (CompHausLike P)ᵒᵖ) : ((topCatToSheafCompHausLike P hs).map f).hom.app x✝ = TypeCat.ofHom fun g => (TopCat.Hom.hom f).comp g
• CompHausLike.LocallyConstant.functorToPresheaves_obj_obj 📋 Mathlib.Condensed.Discrete.LocallyConstant
  {P : TopCat → Prop} (X : Type (max u w)) (x✝ : (CompHausLike P)ᵒᵖ) : (CompHausLike.LocallyConstant.functorToPresheaves.obj X).obj x✝ = match x✝ with | Opposite.op S => LocallyConstant (↑S.toTop) X
• CompHausLike.LocallyConstant.fiber 📋 Mathlib.Condensed.Discrete.LocallyConstant
  {P : TopCat → Prop} [∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), CompHausLike.HasProp P (Subtype p)] {Q : CompHausLike P} {Z : Type (max u w)} (r : LocallyConstant (↑Q.toTop) Z) (a : Function.Fiber ⇑r) : CompHausLike P
• LightCondSet.LocallyConstant.instHasPropAndTotallyDisconnectedSpaceCarrierSecondCountableTopologySubtypeToTop 📋 Mathlib.Condensed.Discrete.LocallyConstant
  (S : LightProfinite) (p : ↑S.toTop → Prop) : CompHausLike.HasProp (fun X => TotallyDisconnectedSpace ↑X ∧ SecondCountableTopology ↑X) (Subtype p)
• CompHausLike.LocallyConstant.sigmaIncl 📋 Mathlib.Condensed.Discrete.LocallyConstant
  {P : TopCat → Prop} [∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), CompHausLike.HasProp P (Subtype p)] {Q : CompHausLike P} {Z : Type (max u w)} (r : LocallyConstant (↑Q.toTop) Z) (a : Function.Fiber ⇑r) : CompHausLike.LocallyConstant.fiber r a ⟶ Q
• CompHausLike.LocallyConstant.counitAppApp 📋 Mathlib.Condensed.Discrete.LocallyConstant
  {P : TopCat → Prop} [∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), CompHausLike.HasProp P (Subtype p)] [CompHausLike.HasProp P PUnit.{u + 1}] (S : CompHausLike P) (Y : CategoryTheory.Functor (CompHausLike P)ᵒᵖ (Type (max u w))) [CategoryTheory.Limits.PreservesFiniteProducts Y] [CompHausLike.HasExplicitFiniteCoproducts P] : LocallyConstant (↑S.toTop) (Y.obj (Opposite.op (CompHausLike.of P PUnit.{u + 1}))) ⟶ Y.obj (Opposite.op S)
• CompHausLike.LocallyConstant.counitApp 📋 Mathlib.Condensed.Discrete.LocallyConstant
  {P : TopCat → Prop} [∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), CompHausLike.HasProp P (Subtype p)] [CompHausLike.HasProp P PUnit.{u + 1}] [CompHausLike.HasExplicitFiniteCoproducts P] (Y : CategoryTheory.Functor (CompHausLike P)ᵒᵖ (Type (max u w))) [CategoryTheory.Limits.PreservesFiniteProducts Y] : CompHausLike.LocallyConstant.functorToPresheaves.obj (Y.obj (Opposite.op (CompHausLike.of P PUnit.{u + 1}))) ⟶ Y
• CompHausLike.LocallyConstant.sigmaIso 📋 Mathlib.Condensed.Discrete.LocallyConstant
  {P : TopCat → Prop} [∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), CompHausLike.HasProp P (Subtype p)] {Q : CompHausLike P} {Z : Type (max u w)} (r : LocallyConstant (↑Q.toTop) Z) [CompHausLike.HasExplicitFiniteCoproducts P] : CompHausLike.finiteCoproduct (CompHausLike.LocallyConstant.fiber r) ≅ Q
• CompHausLike.LocallyConstant.counitApp_app 📋 Mathlib.Condensed.Discrete.LocallyConstant
  {P : TopCat → Prop} [∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), CompHausLike.HasProp P (Subtype p)] [CompHausLike.HasProp P PUnit.{u + 1}] [CompHausLike.HasExplicitFiniteCoproducts P] (Y : CategoryTheory.Functor (CompHausLike P)ᵒᵖ (Type (max u w))) [CategoryTheory.Limits.PreservesFiniteProducts Y] (x✝ : (CompHausLike P)ᵒᵖ) : (CompHausLike.LocallyConstant.counitApp Y).app x✝ = CompHausLike.LocallyConstant.counitAppApp (Opposite.unop x✝) Y
• CompHausLike.LocallyConstant.functorToPresheaves_obj_map 📋 Mathlib.Condensed.Discrete.LocallyConstant
  {P : TopCat → Prop} (X : Type (max u w)) {X✝ Y✝ : (CompHausLike P)ᵒᵖ} (f : X✝ ⟶ Y✝) : (CompHausLike.LocallyConstant.functorToPresheaves.obj X).map f = TypeCat.ofHom fun g => LocallyConstant.comap (TopCat.Hom.hom f.unop.hom) g
• CompHausLike.LocallyConstant.functor 📋 Mathlib.Condensed.Discrete.LocallyConstant
  (P : TopCat → Prop) [CompHausLike.HasExplicitFiniteCoproducts P] [CompHausLike.HasExplicitPullbacks P] (hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), CategoryTheory.EffectiveEpi f → Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f)) : CategoryTheory.Functor (Type (max u w)) (CategoryTheory.Sheaf (CategoryTheory.coherentTopology (CompHausLike P)) (Type (max u w)))
• CompHausLike.LocallyConstant.functorToPresheavesIso 📋 Mathlib.Condensed.Discrete.LocallyConstant
  (P : TopCat → Prop) [CompHausLike.HasExplicitFiniteCoproducts P] [CompHausLike.HasExplicitPullbacks P] (hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), CategoryTheory.EffectiveEpi f → Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f)) (X : Type (max u w)) : CompHausLike.LocallyConstant.functorToPresheaves.obj X ≅ (TopCat.toSheafCompHausLike P (TopCat.discrete.obj X) hs).obj
• CompHausLike.LocallyConstant.counitAppAppImage 📋 Mathlib.Condensed.Discrete.LocallyConstant
  {P : TopCat → Prop} [∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), CompHausLike.HasProp P (Subtype p)] {S : CompHausLike P} {Y : CategoryTheory.Functor (CompHausLike P)ᵒᵖ (Type (max u w))} [CompHausLike.HasProp P PUnit.{u + 1}] (f : LocallyConstant (↑S.toTop) (Y.obj (Opposite.op (CompHausLike.of P PUnit.{u + 1})))) (a : Function.Fiber ⇑f) : Y.obj (Opposite.op (CompHausLike.LocallyConstant.fiber f a))
• CompHausLike.LocallyConstant.functor_obj_obj 📋 Mathlib.Condensed.Discrete.LocallyConstant
  (P : TopCat → Prop) [CompHausLike.HasExplicitFiniteCoproducts P] [CompHausLike.HasExplicitPullbacks P] (hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), CategoryTheory.EffectiveEpi f → Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f)) (X : Type (max u w)) (x✝ : (CompHausLike P)ᵒᵖ) : ((CompHausLike.LocallyConstant.functor P hs).obj X).obj.obj x✝ = LocallyConstant (↑(Opposite.unop x✝).toTop) X
• CompHausLike.LocallyConstant.functor_obj_obj_obj 📋 Mathlib.Condensed.Discrete.LocallyConstant
  (P : TopCat → Prop) [CompHausLike.HasExplicitFiniteCoproducts P] [CompHausLike.HasExplicitPullbacks P] (hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), CategoryTheory.EffectiveEpi f → Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f)) (X : Type (max u w)) (x✝ : (CompHausLike P)ᵒᵖ) : ((CompHausLike.LocallyConstant.functor P hs).obj X).obj.obj x✝ = LocallyConstant (↑(Opposite.unop x✝).toTop) X
• CompHausLike.LocallyConstant.functorIso 📋 Mathlib.Condensed.Discrete.LocallyConstant
  (P : TopCat → Prop) [CompHausLike.HasExplicitFiniteCoproducts P] [CompHausLike.HasExplicitPullbacks P] (hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), CategoryTheory.EffectiveEpi f → Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f)) : CompHausLike.LocallyConstant.functor P hs ≅ TopCat.discrete.comp (topCatToSheafCompHausLike P hs)
• CompHausLike.LocallyConstant.functor_obj_obj_map 📋 Mathlib.Condensed.Discrete.LocallyConstant
  (P : TopCat → Prop) [CompHausLike.HasExplicitFiniteCoproducts P] [CompHausLike.HasExplicitPullbacks P] (hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), CategoryTheory.EffectiveEpi f → Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f)) (X : Type (max u w)) {X✝ Y✝ : (CompHausLike P)ᵒᵖ} (f : X✝ ⟶ Y✝) : ((CompHausLike.LocallyConstant.functor P hs).obj X).obj.map f = TypeCat.ofHom fun g => LocallyConstant.comap (TopCat.Hom.hom f.unop.hom) g
• CompHausLike.LocallyConstant.unitIso 📋 Mathlib.Condensed.Discrete.LocallyConstant
  (P : TopCat → Prop) [CompHausLike.HasProp P PUnit.{u + 1}] [CompHausLike.HasExplicitFiniteCoproducts P] [CompHausLike.HasExplicitPullbacks P] (hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), CategoryTheory.EffectiveEpi f → Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f)) : CategoryTheory.Functor.id (Type (max u w)) ≅ (CompHausLike.LocallyConstant.functor P hs).comp ((CategoryTheory.sheafSections (CategoryTheory.coherentTopology (CompHausLike P)) (Type (max u w))).obj (Opposite.op (CompHausLike.of P PUnit.{u + 1})))
• CompHausLike.LocallyConstant.adjunction 📋 Mathlib.Condensed.Discrete.LocallyConstant
  (P : TopCat → Prop) [∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), CompHausLike.HasProp P (Subtype p)] [CompHausLike.HasProp P PUnit.{u + 1}] [CompHausLike.HasExplicitFiniteCoproducts P] [CompHausLike.HasExplicitPullbacks P] (hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), CategoryTheory.EffectiveEpi f → Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f)) [CompHausLike.HasExplicitFiniteCoproducts P] : CompHausLike.LocallyConstant.functor P hs ⊣ (CategoryTheory.sheafSections (CategoryTheory.coherentTopology (CompHausLike P)) (Type (max u w))).obj (Opposite.op (CompHausLike.of P PUnit.{u + 1}))
• CompHausLike.LocallyConstant.unit 📋 Mathlib.Condensed.Discrete.LocallyConstant
  (P : TopCat → Prop) [CompHausLike.HasProp P PUnit.{u + 1}] [CompHausLike.HasExplicitFiniteCoproducts P] [CompHausLike.HasExplicitPullbacks P] (hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), CategoryTheory.EffectiveEpi f → Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f)) : CategoryTheory.Functor.id (Type (max u u_1)) ⟶ (CompHausLike.LocallyConstant.functor P hs).comp ((CategoryTheory.sheafSections (CategoryTheory.coherentTopology (CompHausLike P)) (Type (max u u_1))).obj (Opposite.op (CompHausLike.of P PUnit.{u + 1})))
• CompHausLike.LocallyConstant.instIsIsoFunctorTypeUnitSheafCoherentTopologyAdjunction 📋 Mathlib.Condensed.Discrete.LocallyConstant
  (P : TopCat → Prop) [∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), CompHausLike.HasProp P (Subtype p)] [CompHausLike.HasProp P PUnit.{u + 1}] [CompHausLike.HasExplicitFiniteCoproducts P] [CompHausLike.HasExplicitPullbacks P] (hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), CategoryTheory.EffectiveEpi f → Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f)) [CompHausLike.HasExplicitFiniteCoproducts P] : CategoryTheory.IsIso (CompHausLike.LocallyConstant.adjunction P hs).unit
• CompHausLike.LocallyConstant.adjunction_unit 📋 Mathlib.Condensed.Discrete.LocallyConstant
  (P : TopCat → Prop) [∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), CompHausLike.HasProp P (Subtype p)] [CompHausLike.HasProp P PUnit.{u + 1}] [CompHausLike.HasExplicitFiniteCoproducts P] [CompHausLike.HasExplicitPullbacks P] (hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), CategoryTheory.EffectiveEpi f → Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f)) [CompHausLike.HasExplicitFiniteCoproducts P] : (CompHausLike.LocallyConstant.adjunction P hs).unit = CompHausLike.LocallyConstant.unit P hs
• CompHausLike.LocallyConstant.componentHom 📋 Mathlib.Condensed.Discrete.LocallyConstant
  {P : TopCat → Prop} [∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), CompHausLike.HasProp P (Subtype p)] {S : CompHausLike P} {Y : CategoryTheory.Functor (CompHausLike P)ᵒᵖ (Type (max u w))} [CompHausLike.HasProp P PUnit.{u + 1}] (f : LocallyConstant (↑S.toTop) (Y.obj (Opposite.op (CompHausLike.of P PUnit.{u + 1})))) {T : CompHausLike P} (g : T ⟶ S) (a : Function.Fiber ⇑(LocallyConstant.comap (TopCat.Hom.hom g.hom) f)) : CompHausLike.LocallyConstant.fiber (LocallyConstant.comap (TopCat.Hom.hom g.hom) f) a ⟶ CompHausLike.LocallyConstant.fiber f (Function.Fiber.mk (⇑f) ((CategoryTheory.ConcreteCategory.hom g) (Function.Fiber.preimage (⇑(LocallyConstant.comap (TopCat.Hom.hom g.hom) f)) a)))
• CompHausLike.LocallyConstant.unit_app 📋 Mathlib.Condensed.Discrete.LocallyConstant
  (P : TopCat → Prop) [CompHausLike.HasProp P PUnit.{u + 1}] [CompHausLike.HasExplicitFiniteCoproducts P] [CompHausLike.HasExplicitPullbacks P] (hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), CategoryTheory.EffectiveEpi f → Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f)) (x✝ : Type (max u u_1)) : (CompHausLike.LocallyConstant.unit P hs).app x✝ = TypeCat.ofHom fun x => LocallyConstant.const (↑(CompHausLike.of P PUnit.{u + 1}).toTop) x
• CompHausLike.LocallyConstant.incl_of_counitAppApp 📋 Mathlib.Condensed.Discrete.LocallyConstant
  {P : TopCat → Prop} [∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), CompHausLike.HasProp P (Subtype p)] {S : CompHausLike P} {Y : CategoryTheory.Functor (CompHausLike P)ᵒᵖ (Type (max u w))} [CompHausLike.HasProp P PUnit.{u + 1}] (f : LocallyConstant (↑S.toTop) (Y.obj (Opposite.op (CompHausLike.of P PUnit.{u + 1})))) [CategoryTheory.Limits.PreservesFiniteProducts Y] [CompHausLike.HasExplicitFiniteCoproducts P] (a : Function.Fiber ⇑f) : (CategoryTheory.ConcreteCategory.hom (Y.map (CompHausLike.LocallyConstant.sigmaIncl f a).op)) ((CategoryTheory.ConcreteCategory.hom (CompHausLike.LocallyConstant.counitAppApp S Y)) f) = CompHausLike.LocallyConstant.counitAppAppImage f a
• CompHausLike.LocallyConstant.functor_map_hom 📋 Mathlib.Condensed.Discrete.LocallyConstant
  (P : TopCat → Prop) [CompHausLike.HasExplicitFiniteCoproducts P] [CompHausLike.HasExplicitPullbacks P] (hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), CategoryTheory.EffectiveEpi f → Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f)) {X✝ Y✝ : Type (max u w)} (f : X✝ ⟶ Y✝) (x✝ : (CompHausLike P)ᵒᵖ) : ((CompHausLike.LocallyConstant.functor P hs).map f).hom.app x✝ = TypeCat.ofHom fun t => LocallyConstant.map (⇑(CategoryTheory.ConcreteCategory.hom f)) t
• CompHausLike.LocallyConstant.functor_map_hom_app 📋 Mathlib.Condensed.Discrete.LocallyConstant
  (P : TopCat → Prop) [CompHausLike.HasExplicitFiniteCoproducts P] [CompHausLike.HasExplicitPullbacks P] (hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), CategoryTheory.EffectiveEpi f → Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f)) {X✝ Y✝ : Type (max u w)} (f : X✝ ⟶ Y✝) (x✝ : (CompHausLike P)ᵒᵖ) : ((CompHausLike.LocallyConstant.functor P hs).map f).hom.app x✝ = TypeCat.ofHom fun t => LocallyConstant.map (⇑(CategoryTheory.ConcreteCategory.hom f)) t
• CompHausLike.LocallyConstant.presheaf_ext 📋 Mathlib.Condensed.Discrete.LocallyConstant
  {P : TopCat → Prop} [∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), CompHausLike.HasProp P (Subtype p)] {S : CompHausLike P} {Y : CategoryTheory.Functor (CompHausLike P)ᵒᵖ (Type (max u w))} [CompHausLike.HasProp P PUnit.{u + 1}] (f : LocallyConstant (↑S.toTop) (Y.obj (Opposite.op (CompHausLike.of P PUnit.{u + 1})))) (X : CategoryTheory.Functor (CompHausLike P)ᵒᵖ (Type (max u w))) [CategoryTheory.Limits.PreservesFiniteProducts X] (x y : X.obj (Opposite.op S)) [CompHausLike.HasExplicitFiniteCoproducts P] (h : ∀ (a : Function.Fiber ⇑f), (CategoryTheory.ConcreteCategory.hom (X.map (CompHausLike.LocallyConstant.sigmaIncl f a).op)) x = (CategoryTheory.ConcreteCategory.hom (X.map (CompHausLike.LocallyConstant.sigmaIncl f a).op)) y) : x = y
• CompHausLike.LocallyConstant.counit 📋 Mathlib.Condensed.Discrete.LocallyConstant
  (P : TopCat → Prop) [∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), CompHausLike.HasProp P (Subtype p)] [CompHausLike.HasProp P PUnit.{u + 1}] [CompHausLike.HasExplicitFiniteCoproducts P] [CompHausLike.HasExplicitPullbacks P] (hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), CategoryTheory.EffectiveEpi f → Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f)) [CompHausLike.HasExplicitFiniteCoproducts P] : ((CategoryTheory.sheafSections (CategoryTheory.coherentTopology (CompHausLike P)) (Type (max u w))).obj (Opposite.op (CompHausLike.of P PUnit.{u + 1}))).comp (CompHausLike.LocallyConstant.functor P hs) ⟶ CategoryTheory.Functor.id (CategoryTheory.Sheaf (CategoryTheory.coherentTopology (CompHausLike P)) (Type (max u w)))
• CompHausLike.LocallyConstant.functorToPresheaves_map_app 📋 Mathlib.Condensed.Discrete.LocallyConstant
  {P : TopCat → Prop} {X✝ Y✝ : Type (max u w)} (f : X✝ ⟶ Y✝) (x✝ : (CompHausLike P)ᵒᵖ) : (CompHausLike.LocallyConstant.functorToPresheaves.map f).app x✝ = TypeCat.ofHom fun t => LocallyConstant.map (⇑(CategoryTheory.ConcreteCategory.hom f)) t
• CompHausLike.LocallyConstant.adjunction_counit 📋 Mathlib.Condensed.Discrete.LocallyConstant
  (P : TopCat → Prop) [∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), CompHausLike.HasProp P (Subtype p)] [CompHausLike.HasProp P PUnit.{u + 1}] [CompHausLike.HasExplicitFiniteCoproducts P] [CompHausLike.HasExplicitPullbacks P] (hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), CategoryTheory.EffectiveEpi f → Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f)) [CompHausLike.HasExplicitFiniteCoproducts P] : (CompHausLike.LocallyConstant.adjunction P hs).counit = CompHausLike.LocallyConstant.counit P hs
• CompHausLike.LocallyConstant.incl_comap 📋 Mathlib.Condensed.Discrete.LocallyConstant
  {P : TopCat → Prop} [∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), CompHausLike.HasProp P (Subtype p)] {Y : CategoryTheory.Functor (CompHausLike P)ᵒᵖ (Type (max u w))} [CompHausLike.HasProp P PUnit.{u + 1}] {S T : (CompHausLike P)ᵒᵖ} (f : LocallyConstant (↑(Opposite.unop S).toTop) (Y.obj (Opposite.op (CompHausLike.of P PUnit.{u + 1})))) (g : S ⟶ T) (a : Function.Fiber ⇑(LocallyConstant.comap (TopCat.Hom.hom g.unop.hom) f)) : CategoryTheory.CategoryStruct.comp g (CompHausLike.LocallyConstant.sigmaIncl (LocallyConstant.comap (TopCat.Hom.hom g.unop.hom) f) a).op = CategoryTheory.CategoryStruct.comp (CompHausLike.LocallyConstant.sigmaIncl f (Function.Fiber.mk (⇑f) ((CategoryTheory.ConcreteCategory.hom g.unop) (Function.Fiber.preimage (⇑(LocallyConstant.comap (TopCat.Hom.hom g.unop.hom) f)) a)))).op (CompHausLike.LocallyConstant.componentHom f g.unop a).op
• CompHausLike.LocallyConstant.adjunction_left_triangle 📋 Mathlib.Condensed.Discrete.LocallyConstant
  (P : TopCat → Prop) [∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), CompHausLike.HasProp P (Subtype p)] [CompHausLike.HasProp P PUnit.{u + 1}] [CompHausLike.HasExplicitFiniteCoproducts P] [CompHausLike.HasExplicitPullbacks P] (hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), CategoryTheory.EffectiveEpi f → Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f)) [CompHausLike.HasExplicitFiniteCoproducts P] (X : Type (max u w)) : CategoryTheory.CategoryStruct.comp (CompHausLike.LocallyConstant.functorToPresheaves.map ((CompHausLike.LocallyConstant.unit P hs).app X)) ((CompHausLike.LocallyConstant.counit P hs).app ((CompHausLike.LocallyConstant.functor P hs).obj X)).hom = CategoryTheory.CategoryStruct.id (CompHausLike.LocallyConstant.functorToPresheaves.obj X)
• CompHausLike.LocallyConstant.sigmaComparison_comp_sigmaIso 📋 Mathlib.Condensed.Discrete.LocallyConstant
  {P : TopCat → Prop} [∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), CompHausLike.HasProp P (Subtype p)] {Q : CompHausLike P} {Z : Type (max u w)} (r : LocallyConstant (↑Q.toTop) Z) (a : Function.Fiber ⇑r) [CompHausLike.HasExplicitFiniteCoproducts P] (X : CategoryTheory.Functor (CompHausLike P)ᵒᵖ (Type (max u w))) : CategoryTheory.CategoryStruct.comp (X.mapIso (CompHausLike.LocallyConstant.sigmaIso r).op).hom (CategoryTheory.CategoryStruct.comp (CompHausLike.sigmaComparison X fun a => ↑(CompHausLike.LocallyConstant.fiber r a).toTop) (TypeCat.ofHom fun g => g a)) = X.map (CompHausLike.LocallyConstant.sigmaIncl r a).op
• CompHausLike.LocallyConstant.counit_app_hom_app_hom_apply 📋 Mathlib.Condensed.Discrete.LocallyConstant
  (P : TopCat → Prop) [∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), CompHausLike.HasProp P (Subtype p)] [CompHausLike.HasProp P PUnit.{u + 1}] [CompHausLike.HasExplicitFiniteCoproducts P] [CompHausLike.HasExplicitPullbacks P] (hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), CategoryTheory.EffectiveEpi f → Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f)) [CompHausLike.HasExplicitFiniteCoproducts P] (X : CategoryTheory.Sheaf (CategoryTheory.coherentTopology (CompHausLike P)) (Type (max u w))) (x✝ : (CompHausLike P)ᵒᵖ) (r : LocallyConstant (↑(Opposite.unop x✝).toTop) (X.obj.obj (Opposite.op (CompHausLike.of P PUnit.{u + 1})))) : (CategoryTheory.ConcreteCategory.hom (((CompHausLike.LocallyConstant.counit P hs).app X).hom.app x✝)) r = (CategoryTheory.ConcreteCategory.hom (X.obj.map (CompHausLike.LocallyConstant.sigmaIso r).inv.op)) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.inv (CompHausLike.sigmaComparison X.obj fun a => ↑↑a))) (CompHausLike.LocallyConstant.counitAppAppImage r))
• LightProfinite.surjective_transitionMapLE 📋 Mathlib.Topology.Category.LightProfinite.AsLimit
  (S : LightProfinite) {n m : ℕ} (h : n ≤ m) : Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (S.transitionMapLE h))
• LightProfinite.surjective_transitionMap 📋 Mathlib.Topology.Category.LightProfinite.AsLimit
  (S : LightProfinite) (n : ℕ) : Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (S.transitionMap n))
• LightProfinite.proj_surjective 📋 Mathlib.Topology.Category.LightProfinite.AsLimit
  (S : LightProfinite) (n : ℕ) : Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (S.proj n))
• LightProfinite.proj_comp_transitionMapLE' 📋 Mathlib.Topology.Category.LightProfinite.AsLimit
  (S : LightProfinite) {n m : ℕ} (h : n ≤ m) : ⇑(CategoryTheory.ConcreteCategory.hom (S.transitionMapLE h)) ∘ ⇑(CategoryTheory.ConcreteCategory.hom (S.proj m)) = ⇑(CategoryTheory.ConcreteCategory.hom (S.proj n))
• LightProfinite.proj_comp_transitionMap' 📋 Mathlib.Topology.Category.LightProfinite.AsLimit
  (S : LightProfinite) (n : ℕ) : ⇑(CategoryTheory.ConcreteCategory.hom (S.transitionMap n)) ∘ ⇑(CategoryTheory.ConcreteCategory.hom (S.proj (n + 1))) = ⇑(CategoryTheory.ConcreteCategory.hom (S.proj n))
• LightProfinite.lightToProfinite_map_proj_eq 📋 Mathlib.Topology.Category.LightProfinite.AsLimit
  (S : LightProfinite) (n : ℕ) : lightToProfinite.map (S.proj n) = (lightToProfinite.obj S).asLimitCone.π.app ((CategoryTheory.Limits.IsCofiltered.sequentialFunctor (DiscreteQuotient ↑(lightToProfinite.obj S).toTop)).obj (Opposite.op n))
• Profinite.instEpiAppDiscreteQuotientCarrierToTopTotallyDisconnectedSpaceπAsLimitCone 📋 Mathlib.Topology.Category.Profinite.Extend
  (S : Profinite) (i : DiscreteQuotient ↑S.toTop) : CategoryTheory.Epi (S.asLimitCone.π.app i)
• Condensed.fintypeCatAsCofan 📋 Mathlib.Condensed.Discrete.Colimit
  (X : Profinite) : CategoryTheory.Limits.Cofan fun x => Profinite.of PUnit.{u + 1}
• Condensed.instPreservesLimitsOfShapeOppositeProfiniteDiscreteCarrierToTopTotallyDisconnectedSpaceOfFinite 📋 Mathlib.Condensed.Discrete.Colimit
  (F : CategoryTheory.Functor Profiniteᵒᵖ (Type (u + 1))) [CategoryTheory.Limits.PreservesFiniteProducts F] (X : Profinite) [Finite ↑X.toTop] : CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete ↑X.toTop) F
• LightCondensed.fintypeCatAsCofan 📋 Mathlib.Condensed.Discrete.Colimit
  (X : LightProfinite) : CategoryTheory.Limits.Cofan fun x => LightProfinite.of PUnit.{u + 1}
• Condensed.fintypeCatAsCofanIsColimit 📋 Mathlib.Condensed.Discrete.Colimit
  (X : Profinite) [Finite ↑X.toTop] : CategoryTheory.Limits.IsColimit (Condensed.fintypeCatAsCofan X)
• Condensed.isoFinYonedaComponents 📋 Mathlib.Condensed.Discrete.Colimit
  (F : CategoryTheory.Functor Profiniteᵒᵖ (Type (u + 1))) [CategoryTheory.Limits.PreservesFiniteProducts F] (X : Profinite) [Finite ↑X.toTop] : F.obj (Opposite.op X) ≅ ↑X.toTop → F.obj (Opposite.op (Profinite.of PUnit.{u + 1}))
• LightCondensed.fintypeCatAsCofanIsColimit 📋 Mathlib.Condensed.Discrete.Colimit
  (X : LightProfinite) [Finite ↑X.toTop] : CategoryTheory.Limits.IsColimit (LightCondensed.fintypeCatAsCofan X)
• LightCondensed.isoFinYonedaComponents 📋 Mathlib.Condensed.Discrete.Colimit
  (F : CategoryTheory.Functor LightProfiniteᵒᵖ (Type u)) [CategoryTheory.Limits.PreservesFiniteProducts F] (X : LightProfinite) [Finite ↑X.toTop] : F.obj (Opposite.op X) ≅ ↑X.toTop → F.obj (Opposite.op (LightProfinite.of PUnit.{u + 1}))
• Condensed.isColimitLocallyConstantPresheafDiagram 📋 Mathlib.Condensed.Discrete.Colimit
  (X : Type (u + 1)) (S : Profinite) : CategoryTheory.Limits.IsColimit ((Condensed.locallyConstantPresheaf X).mapCocone S.asLimitCone.op)
• Condensed.instFinalOppositeDiscreteQuotientCarrierToTopTotallyDisconnectedSpaceCostructuredArrowFintypeCatProfiniteOpToProfiniteOpPtAsLimitConeFunctorOp 📋 Mathlib.Condensed.Discrete.Colimit
  {S : Profinite} : (Profinite.Extend.functorOp S.asLimitCone).Final
• Condensed.lanPresheafNatIso 📋 Mathlib.Condensed.Discrete.Colimit
  {F : CategoryTheory.Functor Profiniteᵒᵖ (Type (u + 1))} (hF : (S : Profinite) → CategoryTheory.Limits.IsColimit (F.mapCocone S.asLimitCone.op)) : Condensed.lanPresheaf F ≅ F
• Condensed.lanPresheafIso 📋 Mathlib.Condensed.Discrete.Colimit
  {S : Profinite} {F : CategoryTheory.Functor Profiniteᵒᵖ (Type (u + 1))} (hF : CategoryTheory.Limits.IsColimit (F.mapCocone S.asLimitCone.op)) : (Condensed.lanPresheaf F).obj (Opposite.op S) ≅ F.obj (Opposite.op S)
• Condensed.isoLocallyConstantOfIsColimit 📋 Mathlib.Condensed.Discrete.Colimit
  (F : CategoryTheory.Functor Profiniteᵒᵖ (Type (u + 1))) [CategoryTheory.Limits.PreservesFiniteProducts F] (hF : (S : Profinite) → CategoryTheory.Limits.IsColimit (F.mapCocone S.asLimitCone.op)) : F ≅ Condensed.locallyConstantPresheaf (F.obj (FintypeCat.toProfinite.op.obj (Opposite.op (FintypeCat.of PUnit.{u + 1}))))
• Condensed.locallyConstantIsoFinYoneda_hom_app 📋 Mathlib.Condensed.Discrete.Colimit
  (F : CategoryTheory.Functor Profiniteᵒᵖ (Type (u + 1))) (X : FintypeCatᵒᵖ) : (Condensed.locallyConstantIsoFinYoneda F).hom.app X = TypeCat.ofHom fun f => ⇑f
• Condensed.isoFinYonedaComponents_hom 📋 Mathlib.Condensed.Discrete.Colimit
  (F : CategoryTheory.Functor Profiniteᵒᵖ (Type (u + 1))) [CategoryTheory.Limits.PreservesFiniteProducts F] (X : Profinite) [Finite ↑X.toTop] : (Condensed.isoFinYonedaComponents F X).hom = TypeCat.ofHom fun y x => (CategoryTheory.ConcreteCategory.hom (F.map (CompHausLike.const (Profinite.of PUnit.{u + 1}) x).op)) y
• Condensed.isoLocallyConstantOfIsColimit_inv 📋 Mathlib.Condensed.Discrete.Colimit
  (X : CategoryTheory.Functor Profiniteᵒᵖ (Type (u + 1))) [CategoryTheory.Limits.PreservesFiniteProducts X] (hX : (S : Profinite) → CategoryTheory.Limits.IsColimit (X.mapCocone S.asLimitCone.op)) : (Condensed.isoLocallyConstantOfIsColimit X hX).inv = CompHausLike.LocallyConstant.counitApp X
• Condensed.lanPresheafIso_hom 📋 Mathlib.Condensed.Discrete.Colimit
  {S : Profinite} {F : CategoryTheory.Functor Profiniteᵒᵖ (Type (u + 1))} (hF : CategoryTheory.Limits.IsColimit (F.mapCocone S.asLimitCone.op)) : (Condensed.lanPresheafIso hF).hom = CategoryTheory.Limits.colimit.desc ((CategoryTheory.CostructuredArrow.proj FintypeCat.toProfinite.op (Opposite.op S)).comp (FintypeCat.toProfinite.op.comp F)) (Profinite.Extend.cocone F S)
• Condensed.lanPresheafNatIso_hom_app 📋 Mathlib.Condensed.Discrete.Colimit
  {F : CategoryTheory.Functor Profiniteᵒᵖ (Type (u + 1))} (hF : (S : Profinite) → CategoryTheory.Limits.IsColimit (F.mapCocone S.asLimitCone.op)) (S : Profiniteᵒᵖ) : (Condensed.lanPresheafNatIso hF).hom.app S = CategoryTheory.Limits.colimit.desc ((CategoryTheory.CostructuredArrow.proj FintypeCat.toProfinite.op (Opposite.op (Opposite.unop S))).comp (FintypeCat.toProfinite.op.comp F)) (Profinite.Extend.cocone F (Opposite.unop S))
• Condensed.isoFinYonedaComponents_hom_apply 📋 Mathlib.Condensed.Discrete.Colimit
  (F : CategoryTheory.Functor Profiniteᵒᵖ (Type (u + 1))) [CategoryTheory.Limits.PreservesFiniteProducts F] (X : Profinite) [Finite ↑X.toTop] (y : F.obj (Opposite.op X)) (x : ↑X.toTop) : (CategoryTheory.ConcreteCategory.hom (Condensed.isoFinYonedaComponents F X).hom) y x = (CategoryTheory.ConcreteCategory.hom (F.map (CompHausLike.const (Profinite.of PUnit.{u + 1}) x).op)) y
• LightCondensed.isoFinYonedaComponents_hom 📋 Mathlib.Condensed.Discrete.Colimit
  (F : CategoryTheory.Functor LightProfiniteᵒᵖ (Type u)) [CategoryTheory.Limits.PreservesFiniteProducts F] (X : LightProfinite) [Finite ↑X.toTop] : (LightCondensed.isoFinYonedaComponents F X).hom = TypeCat.ofHom fun y x => (CategoryTheory.ConcreteCategory.hom (F.map (CompHausLike.const (LightProfinite.of PUnit.{u + 1}) x).op)) y
• LightCondensed.isoFinYonedaComponents_hom_apply 📋 Mathlib.Condensed.Discrete.Colimit
  (F : CategoryTheory.Functor LightProfiniteᵒᵖ (Type u)) [CategoryTheory.Limits.PreservesFiniteProducts F] (X : LightProfinite) [Finite ↑X.toTop] (y : F.obj (Opposite.op X)) (x : ↑X.toTop) : (CategoryTheory.ConcreteCategory.hom (LightCondensed.isoFinYonedaComponents F X).hom) y x = (CategoryTheory.ConcreteCategory.hom (F.map (CompHausLike.const (LightProfinite.of PUnit.{u + 1}) x).op)) y
• Condensed.isoFinYonedaComponents_inv_comp 📋 Mathlib.Condensed.Discrete.Colimit
  (F : CategoryTheory.Functor Profiniteᵒᵖ (Type (u + 1))) [CategoryTheory.Limits.PreservesFiniteProducts F] {X Y : Profinite} [Finite ↑X.toTop] [Finite ↑Y.toTop] (f : ↑Y.toTop → F.obj (Opposite.op (Profinite.of PUnit.{u + 1}))) (g : X ⟶ Y) : (CategoryTheory.ConcreteCategory.hom (Condensed.isoFinYonedaComponents F X).inv) (f ∘ ⇑(CategoryTheory.ConcreteCategory.hom g)) = (CategoryTheory.ConcreteCategory.hom (F.map g.op)) ((CategoryTheory.ConcreteCategory.hom (Condensed.isoFinYonedaComponents F Y).inv) f)
• LightCondensed.isoFinYonedaComponents_inv_comp 📋 Mathlib.Condensed.Discrete.Colimit
  (F : CategoryTheory.Functor LightProfiniteᵒᵖ (Type u)) [CategoryTheory.Limits.PreservesFiniteProducts F] {X Y : LightProfinite} [Finite ↑X.toTop] [Finite ↑Y.toTop] (f : ↑Y.toTop → F.obj (Opposite.op (LightProfinite.of PUnit.{u + 1}))) (g : X ⟶ Y) : (CategoryTheory.ConcreteCategory.hom (LightCondensed.isoFinYonedaComponents F X).inv) (f ∘ ⇑(CategoryTheory.ConcreteCategory.hom g)) = (CategoryTheory.ConcreteCategory.hom (F.map g.op)) ((CategoryTheory.ConcreteCategory.hom (LightCondensed.isoFinYonedaComponents F Y).inv) f)
• LightCondensed.isColimitLocallyConstantPresheafDiagram_desc_apply 📋 Mathlib.Condensed.Discrete.Colimit
  (X : Type u) (S : LightProfinite) (s : CategoryTheory.Limits.Cocone (S.diagram.rightOp.comp (LightCondensed.locallyConstantPresheaf X))) (n : ℕ) (f : LocallyConstant (↑(S.diagram.obj (Opposite.op n)).toTop) X) : (CategoryTheory.ConcreteCategory.hom ((LightCondensed.isColimitLocallyConstantPresheafDiagram X S).desc s)) (LocallyConstant.comap (TopCat.Hom.hom (S.asLimitCone.π.app (Opposite.op n)).hom) f) = (CategoryTheory.ConcreteCategory.hom (s.ι.app n)) f
• Condensed.isColimitLocallyConstantPresheaf_desc_apply 📋 Mathlib.Condensed.Discrete.Colimit
  {I : Type u} [CategoryTheory.Category.{u, u} I] [CategoryTheory.IsCofiltered I] {F : CategoryTheory.Functor I FintypeCat} (c : CategoryTheory.Limits.Cone (F.comp FintypeCat.toProfinite)) (X : Type (u + 1)) (hc : CategoryTheory.Limits.IsLimit c) [∀ (i : I), CategoryTheory.Epi (c.π.app i)] (s : CategoryTheory.Limits.Cocone ((F.comp FintypeCat.toProfinite).op.comp (Condensed.locallyConstantPresheaf X))) (i : I) (f : LocallyConstant (↑(FintypeCat.toProfinite.obj (F.obj i)).toTop) X) : (CategoryTheory.ConcreteCategory.hom ((Condensed.isColimitLocallyConstantPresheaf c X hc).desc s)) (LocallyConstant.comap (TopCat.Hom.hom (c.π.app i).hom) f) = (CategoryTheory.ConcreteCategory.hom (s.ι.app (Opposite.op i))) f
• LightCondensed.isColimitLocallyConstantPresheaf_desc_apply 📋 Mathlib.Condensed.Discrete.Colimit
  {F : CategoryTheory.Functor ℕᵒᵖ FintypeCat} (c : CategoryTheory.Limits.Cone (F.comp FintypeCat.toLightProfinite)) (X : Type u) (hc : CategoryTheory.Limits.IsLimit c) [∀ (i : ℕᵒᵖ), CategoryTheory.Epi (c.π.app i)] (s : CategoryTheory.Limits.Cocone ((F.comp FintypeCat.toLightProfinite).op.comp (LightCondensed.locallyConstantPresheaf X))) (n : ℕᵒᵖ) (f : LocallyConstant (↑(FintypeCat.toLightProfinite.obj (F.obj n)).toTop) X) : (CategoryTheory.ConcreteCategory.hom ((LightCondensed.isColimitLocallyConstantPresheaf c X hc).desc s)) (LocallyConstant.comap (TopCat.Hom.hom (c.π.app n).hom) f) = (CategoryTheory.ConcreteCategory.hom (s.ι.app (Opposite.op n))) f
• Condensed.isoFinYoneda_hom_app_hom_apply 📋 Mathlib.Condensed.Discrete.Colimit
  (F : CategoryTheory.Functor Profiniteᵒᵖ (Type (u + 1))) [CategoryTheory.Limits.PreservesFiniteProducts F] (X : FintypeCatᵒᵖ) (x : (CategoryTheory.Limits.Fan.mk (F.obj (Opposite.op (Condensed.fintypeCatAsCofan (FintypeCat.toProfinite.obj (Opposite.unop X))).pt)) fun j => F.map ((Condensed.fintypeCatAsCofan (FintypeCat.toProfinite.obj (Opposite.unop X))).inj j).op).pt) (j : ↑(FintypeCat.toProfinite.obj (Opposite.unop X)).toTop) : (CategoryTheory.ConcreteCategory.hom ((Condensed.isoFinYoneda F).hom.app X)) x j = (CategoryTheory.ConcreteCategory.hom (F.map ((Condensed.fintypeCatAsCofan (Profinite.of (Opposite.unop X).obj)).inj j).op)) x
• LightCondensed.isoFinYoneda_hom_app_hom_apply 📋 Mathlib.Condensed.Discrete.Colimit
  (F : CategoryTheory.Functor LightProfiniteᵒᵖ (Type u)) [CategoryTheory.Limits.PreservesFiniteProducts F] (X : FintypeCatᵒᵖ) (x : (CategoryTheory.Limits.Fan.mk (F.obj (Opposite.op (LightCondensed.fintypeCatAsCofan (FintypeCat.toLightProfinite.obj (Opposite.unop X))).pt)) fun j => F.map ((LightCondensed.fintypeCatAsCofan (FintypeCat.toLightProfinite.obj (Opposite.unop X))).inj j).op).pt) (j : ↑(FintypeCat.toLightProfinite.obj (Opposite.unop X)).toTop) : (CategoryTheory.ConcreteCategory.hom ((LightCondensed.isoFinYoneda F).hom.app X)) x j = (CategoryTheory.ConcreteCategory.hom (F.map ((LightCondensed.fintypeCatAsCofan (LightProfinite.of (Opposite.unop X).obj)).inj j).op)) x
• Condensed.isColimitLocallyConstantPresheafDiagram_desc_apply 📋 Mathlib.Condensed.Discrete.Colimit
  (X : Type (u + 1)) (S : Profinite) (s : CategoryTheory.Limits.Cocone (S.diagram.op.comp (Condensed.locallyConstantPresheaf X))) (i : DiscreteQuotient ↑S.toTop) (f : LocallyConstant (↑(S.diagram.obj i).toTop) X) : (CategoryTheory.ConcreteCategory.hom ((Condensed.isColimitLocallyConstantPresheafDiagram X S).desc s)) (LocallyConstant.comap (TopCat.Hom.hom (S.asLimitCone.π.app i).hom) f) = (CategoryTheory.ConcreteCategory.hom (s.ι.app (Opposite.op i))) f
• Condensed.isoFinYoneda_inv_app_hom_apply 📋 Mathlib.Condensed.Discrete.Colimit
  (F : CategoryTheory.Functor Profiniteᵒᵖ (Type (u + 1))) [CategoryTheory.Limits.PreservesFiniteProducts F] (X : FintypeCatᵒᵖ) (a✝ : (CategoryTheory.Limits.Types.productLimitCone fun x => F.obj (Opposite.op (Profinite.of PUnit.{u + 1}))).cone.pt) : (CategoryTheory.ConcreteCategory.hom ((Condensed.isoFinYoneda F).inv.app X)) a✝ = (CategoryTheory.CategoryStruct.id (F.obj (Opposite.op (Condensed.fintypeCatAsCofan (Profinite.of (Opposite.unop X).obj)).pt))).hom' ((((CategoryTheory.Limits.IsLimit.postcomposeHomEquiv (CategoryTheory.Discrete.natIso fun j => CategoryTheory.Iso.refl (F.obj (Opposite.op (Profinite.of PUnit.{u + 1})))) (F.mapCone (CategoryTheory.Limits.Fan.mk (Opposite.op (Condensed.fintypeCatAsCofan (Profinite.of (Opposite.unop X).obj)).pt) fun a => ((Condensed.fintypeCatAsCofan (Profinite.of (Opposite.unop X).obj)).inj a).op))).symm (CategoryTheory.Limits.isLimitOfPreserves F (CategoryTheory.Limits.Cofan.IsColimit.op (Condensed.fintypeCatAsCofanIsColimit (Profinite.of (Opposite.unop X).obj))))).lift (CategoryTheory.Limits.Types.productLimitCone fun x => F.obj (Opposite.op (Profinite.of PUnit.{u + 1}))).cone).hom' a✝)
• LightCondensed.isoFinYoneda_inv_app_hom_apply 📋 Mathlib.Condensed.Discrete.Colimit
  (F : CategoryTheory.Functor LightProfiniteᵒᵖ (Type u)) [CategoryTheory.Limits.PreservesFiniteProducts F] (X : FintypeCatᵒᵖ) (a✝ : (CategoryTheory.Limits.Types.productLimitCone fun x => F.obj (Opposite.op (LightProfinite.of PUnit.{u + 1}))).cone.pt) : (CategoryTheory.ConcreteCategory.hom ((LightCondensed.isoFinYoneda F).inv.app X)) a✝ = (CategoryTheory.CategoryStruct.id (F.obj (Opposite.op (LightCondensed.fintypeCatAsCofan (LightProfinite.of (Opposite.unop X).obj)).pt))).hom' ((((CategoryTheory.Limits.IsLimit.postcomposeHomEquiv (CategoryTheory.Discrete.natIso fun j => CategoryTheory.Iso.refl (F.obj (Opposite.op (LightProfinite.of PUnit.{u + 1})))) (F.mapCone (CategoryTheory.Limits.Fan.mk (Opposite.op (LightCondensed.fintypeCatAsCofan (LightProfinite.of (Opposite.unop X).obj)).pt) fun a => ((LightCondensed.fintypeCatAsCofan (LightProfinite.of (Opposite.unop X).obj)).inj a).op))).symm (CategoryTheory.Limits.isLimitOfPreserves F (CategoryTheory.Limits.Cofan.IsColimit.op (LightCondensed.fintypeCatAsCofanIsColimit (LightProfinite.of (Opposite.unop X).obj))))).lift (CategoryTheory.Limits.Types.productLimitCone fun x => F.obj (Opposite.op (LightProfinite.of PUnit.{u + 1}))).cone).hom' a✝)
• CompHausLike.LocallyConstantModule.functorToPresheaves_obj_obj_carrier 📋 Mathlib.Condensed.Discrete.Module
  {P : TopCat → Prop} (R : Type (max u w)) [Ring R] (X : ModuleCat R) (x✝ : (CompHausLike P)ᵒᵖ) : ↑(((CompHausLike.LocallyConstantModule.functorToPresheaves R).obj X).obj x✝) = LocallyConstant ↑(Opposite.unop x✝).toTop ↑X
• CondensedMod.LocallyConstant.functorIsoDiscreteAux₁ 📋 Mathlib.Condensed.Discrete.Module
  (R : Type (u + 1)) [Ring R] (M : ModuleCat R) : M ≅ ModuleCat.of R (LocallyConstant ↑(CompHaus.of PUnit.{u + 1}).toTop ↑M)
• LightCondMod.LocallyConstant.functorIsoDiscreteAux₁ 📋 Mathlib.Condensed.Discrete.Module
  (R : Type u) [Ring R] (M : ModuleCat R) : M ≅ ModuleCat.of R (LocallyConstant ↑(LightProfinite.of PUnit.{u + 1}).toTop ↑M)

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using the Loogle command from the command palette. You can also try the #loogle command from LeanSearchClient, the CLI version, the Loogle VS Code extension, the lean.nvim integration or the Zulip bot.

Usage

Loogle finds definitions and lemmas in various ways:

1. By constant:
   🔍 Real.sin
   finds all lemmas whose statement somehow mentions the sine function.

2. By lemma name substring:
   🔍 "differ"
   finds all lemmas that have "differ" somewhere in their lemma name.

3. By subexpression:
   🔍 _ * (_ ^ _)
   finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

   The pattern can also be non-linear, as in
   🔍 Real.sqrt ?a * Real.sqrt ?a

   If the pattern has parameters, they are matched in any order. Both of these will find List.map:
   🔍 (?a -> ?b) -> List ?a -> List ?b
   🔍 List ?a -> (?a -> ?b) -> List ?b

4. By main conclusion:
   🔍 |- tsum _ = _ * tsum _
   finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

   As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
   🔍 |- _ < _ → tsum _ < tsum _
   will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.

5. You can filter for definitions vs theorems: Using ⊢ (_ : Type _) finds all definitions which provide data while ⊢ (_ : Prop) finds all theorems (and definitions of proofs).

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin and tsum, have "two" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

The #lucky button will directly send you to the documentation of the first hit.

Source code

You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO. Please review the Lean FRO Terms of Use and Privacy Policy.

This is Loogle revision 9f11169 serving mathlib revision 69fae59