Locale

📁 Source: Mathlib/Topology/Category/Locale.lean

Statistics

Metric	Count
Definitions Locale, instCoeSortType, instFrameCarrierUnopFrm, instInhabited, of, instLargeCategoryLocale, topToLocale	7
Theorems faithful, coe_of, topToLocale_map, topToLocale_obj	4
Total	11

CompHausToLocale

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
faithful 📖	mathematical	—	CategoryTheory.Functor.Faithful CompHaus CompHausLike.category Locale instLargeCategoryLocale CategoryTheory.Functor.comp TopCat TopCat.instCategory compHausToTop topToLocale	—	CategoryTheory.ConcreteCategory.ext TopologicalSpace.Opens.comap_injective T3Space.toT0Space T4Space.t3Space instT4SpaceOfT1SpaceOfNormalSpace T2Space.t1Space CompHausLike.instT2SpaceCarrierObjTopCatCompHausLikeToTop NormalSpace.of_regularSpace_lindelofSpace instRegularSpaceOfWeaklyLocallyCompactSpaceOfR1Space instWeaklyLocallyCompactSpaceOfCompactSpace CompHausLike.instCompactSpaceCarrierObjTopCatCompHausLikeToTop T2Space.r1Space instLindelofSpaceOfSigmaCompactSpace CompactSpace.sigmaCompact

Locale

Definitions

Name	Category	Theorems
instCoeSortType 📖	CompOp	—
instFrameCarrierUnopFrm 📖	CompOp	—
instInhabited 📖	CompOp	—
of 📖	CompOp	1 math math: coe_of

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_of 📖	mathematical	—	Frm.carrier Opposite.unop Frm of	—	—

(root)

Definitions

Name	Category	Theorems
Locale 📖	CompOp	3 math math: topToLocale_obj, topToLocale_map, CompHausToLocale.faithful
instLargeCategoryLocale 📖	CompOp	3 math math: topToLocale_obj, topToLocale_map, CompHausToLocale.faithful
topToLocale 📖	CompOp	3 math math: topToLocale_obj, topToLocale_map, CompHausToLocale.faithful

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
topToLocale_map 📖	mathematical	—	CategoryTheory.Functor.map TopCat TopCat.instCategory Locale instLargeCategoryLocale topToLocale Quiver.Hom.op Frm CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Frm.instCategory CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite topCatOpToFrm Opposite.op Frm.ofHom TopologicalSpace.Opens TopCat.carrier TopCat.str TopologicalSpace.Opens.instFrame TopologicalSpace.Opens.comap TopCat.Hom.hom	—	—
topToLocale_obj 📖	mathematical	—	CategoryTheory.Functor.obj TopCat TopCat.instCategory Locale instLargeCategoryLocale topToLocale Opposite.op Frm Opposite CategoryTheory.Category.opposite Frm.instCategory topCatOpToFrm	—	—

---

← Back to Index