Frm

📁 Source: Mathlib/Topology/Category/CompHaus/Frm.lean

Statistics

Metric	Count
Definitions Frm, topCatOpToFrm	2
Theorems faithful, topCatOpToFrm_map, topCatOpToFrm_obj_coe	3
Total	5

CompHausOpToFrame

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
faithful 📖	mathematical	—	CategoryTheory.Functor.Faithful Opposite CompHaus CategoryTheory.Category.opposite CompHausLike.category Frm Frm.instCategory CategoryTheory.Functor.comp TopCat TopCat.instCategory CategoryTheory.Functor.op compHausToTop topCatOpToFrm	—	CategoryTheory.ConcreteCategory.ext TopologicalSpace.Opens.comap_injective T3Space.toT0Space T4Space.t3Space instT4SpaceOfT1SpaceOfNormalSpace T2Space.t1Space CompHaus.instT2SpaceCarrierToTopTrue NormalSpace.of_regularSpace_lindelofSpace instRegularSpaceOfWeaklyLocallyCompactSpaceOfR1Space instWeaklyLocallyCompactSpaceOfCompactSpace CompHaus.instCompactSpaceCarrierToTopTrue T2Space.r1Space instLindelofSpaceOfSigmaCompactSpace CompactSpace.sigmaCompact FrameHom.ext CategoryTheory.congr_fun

(root)

Definitions

Name	Category	Theorems
Frm 📖	CompData	21 math math: Frm.coe_comp, Frm.Iso.mk_hom, topCatOpToFrm_map, Frm.ext_iff, Locale.coe_of, Frm.Iso.mk_inv, topToLocale_obj, Frm.hom_comp, Frm.id_apply, Frm.coe_id, Frm.inv_hom_apply, CompHausOpToFrame.faithful, topCatOpToFrm_obj_coe, Frm.hom_inv_apply, topToLocale_map, Frm.ofHom_comp, Frm.ofHom_id, Frm.hom_id, Frm.ofHom_apply, Frm.comp_apply, Frm.forget_map
topCatOpToFrm 📖	CompOp	5 math math: topCatOpToFrm_map, topToLocale_obj, CompHausOpToFrame.faithful, topCatOpToFrm_obj_coe, topToLocale_map

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
topCatOpToFrm_map 📖	mathematical	—	CategoryTheory.Functor.map Opposite TopCat CategoryTheory.Category.opposite TopCat.instCategory Frm Frm.instCategory topCatOpToFrm Frm.ofHom TopologicalSpace.Opens TopCat.carrier Opposite.unop TopCat.str TopologicalSpace.Opens.instFrame TopologicalSpace.Opens.comap TopCat.Hom.hom Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	—	—
topCatOpToFrm_obj_coe 📖	mathematical	—	Frm.carrier CategoryTheory.Functor.obj Opposite TopCat CategoryTheory.Category.opposite TopCat.instCategory Frm Frm.instCategory topCatOpToFrm TopologicalSpace.Opens TopCat.carrier Opposite.unop TopCat.str	—	—

---

← Back to Index