Loogle!

Result

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

• CompHausLike 📋 Mathlib.Topology.Category.CompHausLike.Basic
  (P : TopCat → Prop) : Type (u + 1)
• CompHausLike.category 📋 Mathlib.Topology.Category.CompHausLike.Basic
  (P : TopCat → Prop) : CategoryTheory.Category.{u, u + 1} (CompHausLike P)
• CompHausLike.toTop 📋 Mathlib.Topology.Category.CompHausLike.Basic
  {P : TopCat → Prop} (self : CompHausLike P) : TopCat
• CompHausLike.instCoeSortType 📋 Mathlib.Topology.Category.CompHausLike.Basic
  (P : TopCat → Prop) : CoeSort (CompHausLike P) (Type u)
• CompHausLike.prop 📋 Mathlib.Topology.Category.CompHausLike.Basic
  {P : TopCat → Prop} (self : CompHausLike P) : P self.toTop
• CompHausLike.compHausLikeToTop 📋 Mathlib.Topology.Category.CompHausLike.Basic
  (P : TopCat → Prop) : CategoryTheory.Functor (CompHausLike P) TopCat
• CompHausLike.fullyFaithfulCompHausLikeToTop 📋 Mathlib.Topology.Category.CompHausLike.Basic
  (P : TopCat → Prop) : (CompHausLike.compHausLikeToTop P).FullyFaithful
• CompHausLike.instFaithfulTopCatCompHausLikeToTop 📋 Mathlib.Topology.Category.CompHausLike.Basic
  (P : TopCat → Prop) : (CompHausLike.compHausLikeToTop P).Faithful
• CompHausLike.instFullTopCatCompHausLikeToTop 📋 Mathlib.Topology.Category.CompHausLike.Basic
  (P : TopCat → Prop) : (CompHausLike.compHausLikeToTop P).Full
• 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.mk 📋 Mathlib.Topology.Category.CompHausLike.Basic
  {P : TopCat → Prop} (toTop : TopCat) [is_compact : CompactSpace ↑toTop] [is_hausdorff : T2Space ↑toTop] (prop : P toTop) : CompHausLike P
• CompHausLike.of 📋 Mathlib.Topology.Category.CompHausLike.Basic
  (P : TopCat → Prop) (X : Type u) [TopologicalSpace X] [CompactSpace X] [T2Space X] [CompHausLike.HasProp P X] : CompHausLike P
• 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.instCompactSpaceCarrierObjTopCatCompHausLikeToTop 📋 Mathlib.Topology.Category.CompHausLike.Basic
  (P : TopCat → Prop) (X : CompHausLike P) : CompactSpace ↑((CompHausLike.compHausLikeToTop P).obj X)
• 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.instT2SpaceCarrierObjTopCatCompHausLikeToTop 📋 Mathlib.Topology.Category.CompHausLike.Basic
  (P : TopCat → Prop) (X : CompHausLike P) : T2Space ↑((CompHausLike.compHausLikeToTop P).obj 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.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)) : CompHausLike.of P X ⟶ CompHausLike.of P Y
• CompHausLike.forget_reflectsIsomorphisms 📋 Mathlib.Topology.Category.CompHausLike.Basic
  {P : TopCat → Prop} : (CategoryTheory.forget (CompHausLike P)).ReflectsIsomorphisms
• CompHausLike.ofHom_id 📋 Mathlib.Topology.Category.CompHausLike.Basic
  (P : TopCat → Prop) {X : Type u} [TopologicalSpace X] [CompactSpace X] [T2Space X] [CompHausLike.HasProp P X] : CompHausLike.ofHom P (ContinuousMap.id X) = CategoryTheory.CategoryStruct.id (CompHausLike.of P X)
• 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.ofHom_comp 📋 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] {Z : Type u} [TopologicalSpace Z] [CompactSpace Z] [T2Space Z] [CompHausLike.HasProp P Z] (f : C(X, Y)) (g : C(Y, Z)) : CompHausLike.ofHom P (g.comp f) = CategoryTheory.CategoryStruct.comp (CompHausLike.ofHom P f) (CompHausLike.ofHom P g)
• 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
• compHausLikeToCompHaus 📋 Mathlib.Topology.Category.CompHaus.Basic
  (P : TopCat → Prop) : CategoryTheory.Functor (CompHausLike P) CompHaus
• CompHaus.epi_iff_surjective 📋 Mathlib.Topology.Category.CompHaus.Basic
  {X Y : CompHaus} (f : X ⟶ Y) : CategoryTheory.Epi f ↔ Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f)
• CompHausLike.HasExplicitFiniteCoproduct 📋 Mathlib.Topology.Category.CompHausLike.Limits
  {P : TopCat → Prop} {α : Type w} (X : α → CompHausLike P) : Prop
• CompHausLike.instHasFiniteCoproductsOfHasExplicitFiniteCoproducts 📋 Mathlib.Topology.Category.CompHausLike.Limits
  {P : TopCat → Prop} [CompHausLike.HasExplicitFiniteCoproducts P] : CategoryTheory.Limits.HasFiniteCoproducts (CompHausLike P)
• CompHausLike.instHasPullbacksOfHasExplicitPullbacks 📋 Mathlib.Topology.Category.CompHausLike.Limits
  {P : TopCat → Prop} [CompHausLike.HasExplicitPullbacks P] : CategoryTheory.Limits.HasPullbacks (CompHausLike P)
• CompHausLike.instFinitaryExtensiveOfHasExplicitPullbacksOfInclusions 📋 Mathlib.Topology.Category.CompHausLike.Limits
  {P : TopCat → Prop} [CompHausLike.HasExplicitFiniteCoproducts P] [CompHausLike.HasExplicitPullbacksOfInclusions P] : CategoryTheory.FinitaryExtensive (CompHausLike P)
• CompHausLike.instPreservesFiniteCoproductsTopCatCompHausLikeToTopOfHasExplicitFiniteCoproducts 📋 Mathlib.Topology.Category.CompHausLike.Limits
  (P : TopCat → Prop) [CompHausLike.HasExplicitFiniteCoproducts P] : CategoryTheory.Limits.PreservesFiniteCoproducts (CompHausLike.compHausLikeToTop P)
• CompHausLike.finiteCoproduct 📋 Mathlib.Topology.Category.CompHausLike.Limits
  {P : TopCat → Prop} {α : Type w} [Finite α] (X : α → CompHausLike P) [CompHausLike.HasExplicitFiniteCoproduct X] : CompHausLike P
• CompHausLike.HasExplicitFiniteCoproducts.hasProp 📋 Mathlib.Topology.Category.CompHausLike.Limits
  {P : TopCat → Prop} [self : CompHausLike.HasExplicitFiniteCoproducts P] {α : Type w} [Finite α] (X : α → CompHausLike P) : CompHausLike.HasExplicitFiniteCoproduct X
• CompHausLike.HasExplicitFiniteCoproducts.mk 📋 Mathlib.Topology.Category.CompHausLike.Limits
  {P : TopCat → Prop} (hasProp : ∀ {α : Type w} [Finite α] (X : α → CompHausLike P), CompHausLike.HasExplicitFiniteCoproduct X) : CompHausLike.HasExplicitFiniteCoproducts P
• CompHausLike.instHasColimitsOfShapeDiscreteOfHasExplicitFiniteCoproductsOfFinite 📋 Mathlib.Topology.Category.CompHausLike.Limits
  {P : TopCat → Prop} [CompHausLike.HasExplicitFiniteCoproducts P] (α : Type w) [Finite α] : CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete α) (CompHausLike P)
• CompHausLike.instHasCoproduct 📋 Mathlib.Topology.Category.CompHausLike.Limits
  {P : TopCat → Prop} {α : Type w} [Finite α] (X : α → CompHausLike P) [CompHausLike.HasExplicitFiniteCoproduct X] : CategoryTheory.Limits.HasCoproduct X
• CompHausLike.instHasPullbacksOfInclusionsOfHasExplicitPullbacksOfInclusions 📋 Mathlib.Topology.Category.CompHausLike.Limits
  {P : TopCat → Prop} [CompHausLike.HasExplicitFiniteCoproducts P] [CompHausLike.HasExplicitPullbacksOfInclusions P] : CategoryTheory.HasPullbacksOfInclusions (CompHausLike P)
• CompHausLike.finiteCoproduct.cofan 📋 Mathlib.Topology.Category.CompHausLike.Limits
  {P : TopCat → Prop} {α : Type w} [Finite α] (X : α → CompHausLike P) [CompHausLike.HasExplicitFiniteCoproduct X] : CategoryTheory.Limits.Cofan X
• CompHausLike.instPreservesPullbacksOfInclusionsTopCatCompHausLikeToTopOfHasExplicitPullbacksOfInclusions 📋 Mathlib.Topology.Category.CompHausLike.Limits
  {P : TopCat → Prop} [CompHausLike.HasExplicitFiniteCoproducts P] [CompHausLike.HasExplicitPullbacksOfInclusions P] : CategoryTheory.PreservesPullbacksOfInclusions (CompHausLike.compHausLikeToTop P)
• CompHausLike.isTerminalPUnit 📋 Mathlib.Topology.Category.CompHausLike.Limits
  {P : TopCat → Prop} [CompHausLike.HasProp P PUnit.{u + 1}] : CategoryTheory.Limits.IsTerminal (CompHausLike.of P PUnit.{u + 1})
• 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.finiteCoproduct.ι 📋 Mathlib.Topology.Category.CompHausLike.Limits
  {P : TopCat → Prop} {α : Type w} [Finite α] (X : α → CompHausLike P) [CompHausLike.HasExplicitFiniteCoproduct X] (a : α) : X a ⟶ CompHausLike.finiteCoproduct X
• CompHausLike.finiteCoproduct.isColimit 📋 Mathlib.Topology.Category.CompHausLike.Limits
  {P : TopCat → Prop} {α : Type w} [Finite α] (X : α → CompHausLike P) [CompHausLike.HasExplicitFiniteCoproduct X] : CategoryTheory.Limits.IsColimit (CompHausLike.finiteCoproduct.cofan X)
• CompHausLike.HasExplicitPullback 📋 Mathlib.Topology.Category.CompHausLike.Limits
  {P : TopCat → Prop} {X Y B : CompHausLike P} (f : X ⟶ B) (g : Y ⟶ B) : Prop
• CompHausLike.pullback 📋 Mathlib.Topology.Category.CompHausLike.Limits
  {P : TopCat → Prop} {X Y B : CompHausLike P} (f : X ⟶ B) (g : Y ⟶ B) [CompHausLike.HasExplicitPullback f g] : CompHausLike P
• CompHausLike.HasExplicitPullbacks.hasProp 📋 Mathlib.Topology.Category.CompHausLike.Limits
  {P : TopCat → Prop} [self : CompHausLike.HasExplicitPullbacks P] {X Y B : CompHausLike P} (f : X ⟶ B) (g : Y ⟶ B) : CompHausLike.HasExplicitPullback f g
• CompHausLike.HasExplicitPullbacks.mk 📋 Mathlib.Topology.Category.CompHausLike.Limits
  {P : TopCat → Prop} (hasProp : ∀ {X Y B : CompHausLike P} (f : X ⟶ B) (g : Y ⟶ B), CompHausLike.HasExplicitPullback f g) : CompHausLike.HasExplicitPullbacks P
• CompHausLike.finiteCoproduct.desc 📋 Mathlib.Topology.Category.CompHausLike.Limits
  {P : TopCat → Prop} {α : Type w} [Finite α] (X : α → CompHausLike P) [CompHausLike.HasExplicitFiniteCoproduct X] {B : CompHausLike P} (e : (a : α) → X a ⟶ B) : CompHausLike.finiteCoproduct X ⟶ B
• CompHausLike.pullback.cone 📋 Mathlib.Topology.Category.CompHausLike.Limits
  {P : TopCat → Prop} {X Y B : CompHausLike P} (f : X ⟶ B) (g : Y ⟶ B) [CompHausLike.HasExplicitPullback f g] : CategoryTheory.Limits.PullbackCone f g
• CompHausLike.instHasLimitWalkingCospanCospan 📋 Mathlib.Topology.Category.CompHausLike.Limits
  {P : TopCat → Prop} {X Y B : CompHausLike P} (f : X ⟶ B) (g : Y ⟶ B) [CompHausLike.HasExplicitPullback f g] : CategoryTheory.Limits.HasLimit (CategoryTheory.Limits.cospan f g)
• CompHausLike.pullback.fst 📋 Mathlib.Topology.Category.CompHausLike.Limits
  {P : TopCat → Prop} {X Y B : CompHausLike P} (f : X ⟶ B) (g : Y ⟶ B) [CompHausLike.HasExplicitPullback f g] : CompHausLike.pullback f g ⟶ X
• CompHausLike.pullback.snd 📋 Mathlib.Topology.Category.CompHausLike.Limits
  {P : TopCat → Prop} {X Y B : CompHausLike P} (f : X ⟶ B) (g : Y ⟶ B) [CompHausLike.HasExplicitPullback f g] : CompHausLike.pullback f g ⟶ Y
• CompHausLike.instCreatesLimitTopCatWalkingCospanCospanCompHausLikeToTop 📋 Mathlib.Topology.Category.CompHausLike.Limits
  {P : TopCat → Prop} {X Y B : CompHausLike P} (f : X ⟶ B) (g : Y ⟶ B) [CompHausLike.HasExplicitPullback f g] : CategoryTheory.CreatesLimit (CategoryTheory.Limits.cospan f g) (CompHausLike.compHausLikeToTop P)
• CompHausLike.instPreservesLimitTopCatWalkingCospanCospanCompHausLikeToTop 📋 Mathlib.Topology.Category.CompHausLike.Limits
  {P : TopCat → Prop} {X Y B : CompHausLike P} (f : X ⟶ B) (g : Y ⟶ B) [CompHausLike.HasExplicitPullback f g] : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f g) (CompHausLike.compHausLikeToTop P)
• CompHausLike.pullback.isLimit 📋 Mathlib.Topology.Category.CompHausLike.Limits
  {P : TopCat → Prop} {X Y B : CompHausLike P} (f : X ⟶ B) (g : Y ⟶ B) [CompHausLike.HasExplicitPullback f g] : CategoryTheory.Limits.IsLimit (CompHausLike.pullback.cone f g)
• CompHausLike.pullback.cone_pt 📋 Mathlib.Topology.Category.CompHausLike.Limits
  {P : TopCat → Prop} {X Y B : CompHausLike P} (f : X ⟶ B) (g : Y ⟶ B) [CompHausLike.HasExplicitPullback f g] : (CompHausLike.pullback.cone f g).pt = CompHausLike.pullback f g
• 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.ι_desc 📋 Mathlib.Topology.Category.CompHausLike.Limits
  {P : TopCat → Prop} {α : Type w} [Finite α] (X : α → CompHausLike P) [CompHausLike.HasExplicitFiniteCoproduct X] {B : CompHausLike P} (e : (a : α) → X a ⟶ B) (a : α) : CategoryTheory.CategoryStruct.comp (CompHausLike.finiteCoproduct.ι X a) (CompHausLike.finiteCoproduct.desc X e) = e a
• CompHausLike.pullback.condition 📋 Mathlib.Topology.Category.CompHausLike.Limits
  {P : TopCat → Prop} {X Y B : CompHausLike P} (f : X ⟶ B) (g : Y ⟶ B) [CompHausLike.HasExplicitPullback f g] : CategoryTheory.CategoryStruct.comp (CompHausLike.pullback.fst f g) f = CategoryTheory.CategoryStruct.comp (CompHausLike.pullback.snd f g) g
• CompHausLike.HasExplicitPullbacksOfInclusions.hasProp 📋 Mathlib.Topology.Category.CompHausLike.Limits
  {P : TopCat → Prop} {inst✝ : CompHausLike.HasExplicitFiniteCoproducts P} [self : CompHausLike.HasExplicitPullbacksOfInclusions P] {X Y Z : CompHausLike P} (f : Z ⟶ X ⨿ Y) : CompHausLike.HasExplicitPullback CategoryTheory.Limits.coprod.inl f
• CompHausLike.HasExplicitPullbacksOfInclusions.mk 📋 Mathlib.Topology.Category.CompHausLike.Limits
  {P : TopCat → Prop} [CompHausLike.HasExplicitFiniteCoproducts P] (hasProp : ∀ {X Y Z : CompHausLike P} (f : Z ⟶ X ⨿ Y), CompHausLike.HasExplicitPullback CategoryTheory.Limits.coprod.inl f) : CompHausLike.HasExplicitPullbacksOfInclusions P
• CompHausLike.finiteCoproduct.ι_desc_assoc 📋 Mathlib.Topology.Category.CompHausLike.Limits
  {P : TopCat → Prop} {α : Type w} [Finite α] (X : α → CompHausLike P) [CompHausLike.HasExplicitFiniteCoproduct X] {B : CompHausLike P} (e : (a : α) → X a ⟶ B) (a : α) {Z : CompHausLike P} (h : B ⟶ Z) : CategoryTheory.CategoryStruct.comp (CompHausLike.finiteCoproduct.ι X a) (CategoryTheory.CategoryStruct.comp (CompHausLike.finiteCoproduct.desc X e) h) = CategoryTheory.CategoryStruct.comp (e a) h
• CompHausLike.pullback.lift 📋 Mathlib.Topology.Category.CompHausLike.Limits
  {P : TopCat → Prop} {X Y B : CompHausLike P} (f : X ⟶ B) (g : Y ⟶ B) [CompHausLike.HasExplicitPullback f g] {Z : CompHausLike P} (a : Z ⟶ X) (b : Z ⟶ Y) (w : CategoryTheory.CategoryStruct.comp a f = CategoryTheory.CategoryStruct.comp b g) : Z ⟶ CompHausLike.pullback f g
• CompHausLike.finiteCoproduct.hom_ext 📋 Mathlib.Topology.Category.CompHausLike.Limits
  {P : TopCat → Prop} {α : Type w} [Finite α] (X : α → CompHausLike P) [CompHausLike.HasExplicitFiniteCoproduct X] {B : CompHausLike P} (f g : CompHausLike.finiteCoproduct X ⟶ B) (h : ∀ (a : α), CategoryTheory.CategoryStruct.comp (CompHausLike.finiteCoproduct.ι X a) f = CategoryTheory.CategoryStruct.comp (CompHausLike.finiteCoproduct.ι X a) g) : f = g
• CompHausLike.pullback.condition_assoc 📋 Mathlib.Topology.Category.CompHausLike.Limits
  {P : TopCat → Prop} {X Y B : CompHausLike P} (f : X ⟶ B) (g : Y ⟶ B) [CompHausLike.HasExplicitPullback f g] {Z : CompHausLike P} (h : B ⟶ Z) : CategoryTheory.CategoryStruct.comp (CompHausLike.pullback.fst f g) (CategoryTheory.CategoryStruct.comp f h) = CategoryTheory.CategoryStruct.comp (CompHausLike.pullback.snd f g) (CategoryTheory.CategoryStruct.comp g h)
• CompHausLike.pullback.lift_fst 📋 Mathlib.Topology.Category.CompHausLike.Limits
  {P : TopCat → Prop} {X Y B : CompHausLike P} (f : X ⟶ B) (g : Y ⟶ B) [CompHausLike.HasExplicitPullback f g] {Z : CompHausLike P} (a : Z ⟶ X) (b : Z ⟶ Y) (w : CategoryTheory.CategoryStruct.comp a f = CategoryTheory.CategoryStruct.comp b g) : CategoryTheory.CategoryStruct.comp (CompHausLike.pullback.lift f g a b w) (CompHausLike.pullback.fst f g) = a
• CompHausLike.pullback.lift_snd 📋 Mathlib.Topology.Category.CompHausLike.Limits
  {P : TopCat → Prop} {X Y B : CompHausLike P} (f : X ⟶ B) (g : Y ⟶ B) [CompHausLike.HasExplicitPullback f g] {Z : CompHausLike P} (a : Z ⟶ X) (b : Z ⟶ Y) (w : CategoryTheory.CategoryStruct.comp a f = CategoryTheory.CategoryStruct.comp b g) : CategoryTheory.CategoryStruct.comp (CompHausLike.pullback.lift f g a b w) (CompHausLike.pullback.snd f g) = b
• CompHausLike.pullback.isLimit_lift 📋 Mathlib.Topology.Category.CompHausLike.Limits
  {P : TopCat → Prop} {X Y B : CompHausLike P} (f : X ⟶ B) (g : Y ⟶ B) [CompHausLike.HasExplicitPullback f g] (s : CategoryTheory.Limits.PullbackCone f g) : (CompHausLike.pullback.isLimit f g).lift s = CompHausLike.pullback.lift f g s.fst s.snd ⋯
• 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.pullback.lift_fst_assoc 📋 Mathlib.Topology.Category.CompHausLike.Limits
  {P : TopCat → Prop} {X Y B : CompHausLike P} (f : X ⟶ B) (g : Y ⟶ B) [CompHausLike.HasExplicitPullback f g] {Z : CompHausLike P} (a : Z ⟶ X) (b : Z ⟶ Y) (w : CategoryTheory.CategoryStruct.comp a f = CategoryTheory.CategoryStruct.comp b g) {Z✝ : CompHausLike P} (h : X ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CompHausLike.pullback.lift f g a b w) (CategoryTheory.CategoryStruct.comp (CompHausLike.pullback.fst f g) h) = CategoryTheory.CategoryStruct.comp a h
• CompHausLike.pullback.lift_snd_assoc 📋 Mathlib.Topology.Category.CompHausLike.Limits
  {P : TopCat → Prop} {X Y B : CompHausLike P} (f : X ⟶ B) (g : Y ⟶ B) [CompHausLike.HasExplicitPullback f g] {Z : CompHausLike P} (a : Z ⟶ X) (b : Z ⟶ Y) (w : CategoryTheory.CategoryStruct.comp a f = CategoryTheory.CategoryStruct.comp b g) {Z✝ : CompHausLike P} (h : Y ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CompHausLike.pullback.lift f g a b w) (CategoryTheory.CategoryStruct.comp (CompHausLike.pullback.snd f g) h) = CategoryTheory.CategoryStruct.comp b h
• CompHausLike.pullback.hom_ext 📋 Mathlib.Topology.Category.CompHausLike.Limits
  {P : TopCat → Prop} {X Y B : CompHausLike P} (f : X ⟶ B) (g : Y ⟶ B) [CompHausLike.HasExplicitPullback f g] {Z : CompHausLike P} (a b : Z ⟶ CompHausLike.pullback f g) (hfst : CategoryTheory.CategoryStruct.comp a (CompHausLike.pullback.fst f g) = CategoryTheory.CategoryStruct.comp b (CompHausLike.pullback.fst f g)) (hsnd : CategoryTheory.CategoryStruct.comp a (CompHausLike.pullback.snd f g) = CategoryTheory.CategoryStruct.comp b (CompHausLike.pullback.snd f g)) : a = b
• 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.pullback.cone_π 📋 Mathlib.Topology.Category.CompHausLike.Limits
  {P : TopCat → Prop} {X Y B : CompHausLike P} (f : X ⟶ B) (g : Y ⟶ B) [CompHausLike.HasExplicitPullback f g] : (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 := ⋯ }
• 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.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)
• 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.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
• 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.sigmaComparison 📋 Mathlib.Topology.Category.CompHausLike.SigmaComparison
  {P : TopCat → Prop} [CompHausLike.HasExplicitFiniteCoproducts P] (X : CategoryTheory.Functor (CompHausLike P)ᵒᵖ (Type (max u w))) {α : Type u} [Finite α] (σ : α → Type u) [(a : α) → TopologicalSpace (σ a)] [∀ (a : α), CompactSpace (σ a)] [∀ (a : α), T2Space (σ a)] [∀ (a : α), CompHausLike.HasProp P (σ a)] : X.obj (Opposite.op (CompHausLike.of P ((a : α) × σ a))) ⟶ (a : α) → X.obj (Opposite.op (CompHausLike.of P (σ a)))
• CompHausLike.isIsoSigmaComparison 📋 Mathlib.Topology.Category.CompHausLike.SigmaComparison
  {P : TopCat → Prop} [CompHausLike.HasExplicitFiniteCoproducts P] (X : CategoryTheory.Functor (CompHausLike P)ᵒᵖ (Type (max u w))) [CategoryTheory.Limits.PreservesFiniteProducts X] {α : Type u} [Finite α] (σ : α → Type u) [(a : α) → TopologicalSpace (σ a)] [∀ (a : α), CompactSpace (σ a)] [∀ (a : α), T2Space (σ a)] [∀ (a : α), CompHausLike.HasProp P (σ a)] : CategoryTheory.IsIso (CompHausLike.sigmaComparison X σ)
• CompHausLike.sigmaComparison_eq_comp_isos 📋 Mathlib.Topology.Category.CompHausLike.SigmaComparison
  {P : TopCat → Prop} [CompHausLike.HasExplicitFiniteCoproducts P] (X : CategoryTheory.Functor (CompHausLike P)ᵒᵖ (Type (max u w))) [CategoryTheory.Limits.PreservesFiniteProducts X] {α : Type u} [Finite α] (σ : α → Type u) [(a : α) → TopologicalSpace (σ a)] [∀ (a : α), CompactSpace (σ a)] [∀ (a : α), T2Space (σ a)] [∀ (a : α), CompHausLike.HasProp P (σ a)] : CompHausLike.sigmaComparison X σ = CategoryTheory.CategoryStruct.comp (X.mapIso (CategoryTheory.Limits.opCoproductIsoProduct' (CompHausLike.finiteCoproduct.isColimit fun a => CompHausLike.of P (σ a)) (CategoryTheory.Limits.productIsProduct fun x => Opposite.op (CompHausLike.of P (σ x))))).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.PreservesProduct.iso X fun a => Opposite.op (CompHausLike.of P (σ a))).hom (CategoryTheory.Limits.Types.productIso fun a => X.obj (Opposite.op (CompHausLike.of P (σ a)))).hom)
• CompHausLike.LocallyConstant.functorToPresheaves 📋 Mathlib.Condensed.Discrete.LocallyConstant
  {P : TopCat → Prop} : CategoryTheory.Functor (Type (max u w)) (CategoryTheory.Functor (CompHausLike P)ᵒᵖ (Type (max u w)))
• 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
• 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))
• 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.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.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
• CompHausLike.LocallyConstantModule.functorToPresheaves 📋 Mathlib.Condensed.Discrete.Module
  {P : TopCat → Prop} (R : Type (max u w)) [Ring R] : CategoryTheory.Functor (ModuleCat R) (CategoryTheory.Functor (CompHausLike P)ᵒᵖ (ModuleCat R))
• 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

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