AlexDisc

📁 Source: Mathlib/Topology/Order/Category/AlexDisc.lean

Statistics

Metric	Count
Definitions AlexDisc, mk, category, concreteCategory, instCoeSortType, instHasForgetToTop, of, toTopCat, alexDiscEquivPreord	9
Theorems mk_hom, mk_inv, coe_forgetToTop, coe_of, forgetToTop_faithful, forgetToTop_full, forgetToTop_of, is_alexandrovDiscrete, alexDiscEquivPreord_counitIso, alexDiscEquivPreord_functor, alexDiscEquivPreord_inverse_map, alexDiscEquivPreord_inverse_obj_carrier, alexDiscEquivPreord_inverse_obj_str, alexDiscEquivPreord_unitIso	14
Total	23

AlexDisc

Definitions

Name	Category	Theorems
category 📖	CompOp	12 math math: alexDiscEquivPreord_inverse_obj_carrier, alexDiscEquivPreord_inverse_obj_str, alexDiscEquivPreord_inverse_map, forgetToTop_faithful, Iso.mk_inv, alexDiscEquivPreord_unitIso, coe_forgetToTop, forgetToTop_full, Iso.mk_hom, alexDiscEquivPreord_counitIso, forgetToTop_of, alexDiscEquivPreord_functor
concreteCategory 📖	CompOp	10 math math: alexDiscEquivPreord_inverse_map, forgetToTop_faithful, Iso.mk_inv, alexDiscEquivPreord_unitIso, coe_forgetToTop, forgetToTop_full, Iso.mk_hom, alexDiscEquivPreord_counitIso, forgetToTop_of, alexDiscEquivPreord_functor
instCoeSortType 📖	CompOp	—
instHasForgetToTop 📖	CompOp	7 math math: forgetToTop_faithful, alexDiscEquivPreord_unitIso, coe_forgetToTop, forgetToTop_full, alexDiscEquivPreord_counitIso, forgetToTop_of, alexDiscEquivPreord_functor
of 📖	CompOp	5 math math: alexDiscEquivPreord_inverse_map, alexDiscEquivPreord_unitIso, alexDiscEquivPreord_counitIso, coe_of, forgetToTop_of
toTopCat 📖	CompOp	14 math math: alexDiscEquivPreord_inverse_obj_carrier, alexDiscEquivPreord_inverse_obj_str, alexDiscEquivPreord_inverse_map, forgetToTop_faithful, Iso.mk_inv, alexDiscEquivPreord_unitIso, coe_forgetToTop, forgetToTop_full, Iso.mk_hom, is_alexandrovDiscrete, alexDiscEquivPreord_counitIso, coe_of, forgetToTop_of, alexDiscEquivPreord_functor

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_forgetToTop 📖	mathematical	—	TopCat.carrier CategoryTheory.Functor.obj AlexDisc category TopCat TopCat.instCategory CategoryTheory.forget₂ ContinuousMap toTopCat TopCat.str ContinuousMap.instFunLike concreteCategory TopCat.instConcreteCategoryContinuousMapCarrier instHasForgetToTop	—	—
coe_of 📖	mathematical	—	TopCat.carrier toTopCat of	—	—
forgetToTop_faithful 📖	mathematical	—	CategoryTheory.Functor.Faithful AlexDisc category TopCat TopCat.instCategory CategoryTheory.forget₂ ContinuousMap TopCat.carrier toTopCat TopCat.str ContinuousMap.instFunLike concreteCategory TopCat.instConcreteCategoryContinuousMapCarrier instHasForgetToTop	—	CategoryTheory.ConcreteCategory.ext ContinuousMap.ext CategoryTheory.ConcreteCategory.congr_hom
forgetToTop_full 📖	mathematical	—	CategoryTheory.Functor.Full AlexDisc category TopCat TopCat.instCategory CategoryTheory.forget₂ ContinuousMap TopCat.carrier toTopCat TopCat.str ContinuousMap.instFunLike concreteCategory TopCat.instConcreteCategoryContinuousMapCarrier instHasForgetToTop	—	—
forgetToTop_of 📖	mathematical	—	CategoryTheory.Functor.obj AlexDisc category TopCat TopCat.instCategory CategoryTheory.forget₂ ContinuousMap TopCat.carrier toTopCat TopCat.str ContinuousMap.instFunLike concreteCategory TopCat.instConcreteCategoryContinuousMapCarrier instHasForgetToTop of TopCat.of	—	—
is_alexandrovDiscrete 📖	mathematical	—	AlexandrovDiscrete TopCat.carrier toTopCat TopCat.str	—	—

AlexDisc.Iso

Definitions

Name	Category	Theorems
mk 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mk_hom 📖	mathematical	—	CategoryTheory.Iso.hom AlexDisc AlexDisc.category CategoryTheory.ConcreteCategory.ofHom ContinuousMap TopCat.carrier AlexDisc.toTopCat TopCat.str ContinuousMap.instFunLike AlexDisc.concreteCategory toContinuousMap Homeomorph EquivLike.toFunLike Homeomorph.instEquivLike	—	—
mk_inv 📖	mathematical	—	CategoryTheory.Iso.inv AlexDisc AlexDisc.category CategoryTheory.ConcreteCategory.ofHom ContinuousMap TopCat.carrier AlexDisc.toTopCat TopCat.str ContinuousMap.instFunLike AlexDisc.concreteCategory toContinuousMap Homeomorph EquivLike.toFunLike Homeomorph.instEquivLike Homeomorph.symm	—	—

(root)

Definitions

Name	Category	Theorems
AlexDisc 📖	CompData	12 math math: alexDiscEquivPreord_inverse_obj_carrier, alexDiscEquivPreord_inverse_obj_str, alexDiscEquivPreord_inverse_map, AlexDisc.forgetToTop_faithful, AlexDisc.Iso.mk_inv, alexDiscEquivPreord_unitIso, AlexDisc.coe_forgetToTop, AlexDisc.forgetToTop_full, AlexDisc.Iso.mk_hom, alexDiscEquivPreord_counitIso, AlexDisc.forgetToTop_of, alexDiscEquivPreord_functor
alexDiscEquivPreord 📖	CompOp	6 math math: alexDiscEquivPreord_inverse_obj_carrier, alexDiscEquivPreord_inverse_obj_str, alexDiscEquivPreord_inverse_map, alexDiscEquivPreord_unitIso, alexDiscEquivPreord_counitIso, alexDiscEquivPreord_functor

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
alexDiscEquivPreord_counitIso 📖	mathematical	—	CategoryTheory.Equivalence.counitIso AlexDisc Preord AlexDisc.category Preord.instCategory alexDiscEquivPreord CategoryTheory.NatIso.ofComponents CategoryTheory.Functor.comp AlexDisc.of Topology.WithUpperSet Preord.carrier Topology.WithUpperSet.instTopologicalSpace Preord.str CategoryTheory.ConcreteCategory.ofHom ContinuousMap TopCat.carrier AlexDisc.toTopCat TopCat.str ContinuousMap.instFunLike AlexDisc.concreteCategory Topology.WithUpperSet.map Preord.Hom.hom TopCat TopCat.instCategory CategoryTheory.forget₂ TopCat.instConcreteCategoryContinuousMapCarrier AlexDisc.instHasForgetToTop topToPreord CategoryTheory.Functor.id CategoryTheory.Functor.obj OrderIso Preorder.toLE OrderIso.symm Specialization Specialization.instPreorder orderIsoSpecializationWithUpperSetTopology	—	—
alexDiscEquivPreord_functor 📖	mathematical	—	CategoryTheory.Equivalence.functor AlexDisc Preord AlexDisc.category Preord.instCategory alexDiscEquivPreord CategoryTheory.Functor.comp TopCat TopCat.instCategory CategoryTheory.forget₂ ContinuousMap TopCat.carrier AlexDisc.toTopCat TopCat.str ContinuousMap.instFunLike AlexDisc.concreteCategory TopCat.instConcreteCategoryContinuousMapCarrier AlexDisc.instHasForgetToTop topToPreord	—	—
alexDiscEquivPreord_inverse_map 📖	mathematical	—	CategoryTheory.Functor.map Preord Preord.instCategory AlexDisc AlexDisc.category CategoryTheory.Equivalence.inverse alexDiscEquivPreord CategoryTheory.ConcreteCategory.ofHom ContinuousMap TopCat.carrier AlexDisc.toTopCat TopCat.str ContinuousMap.instFunLike AlexDisc.concreteCategory AlexDisc.of Topology.WithUpperSet Preord.carrier Topology.WithUpperSet.instTopologicalSpace Preord.str Topology.WithUpperSet.map Preord.Hom.hom	—	—
alexDiscEquivPreord_inverse_obj_carrier 📖	mathematical	—	TopCat.carrier AlexDisc.toTopCat CategoryTheory.Functor.obj Preord Preord.instCategory AlexDisc AlexDisc.category CategoryTheory.Equivalence.inverse alexDiscEquivPreord Topology.WithUpperSet Preord.carrier	—	—
alexDiscEquivPreord_inverse_obj_str 📖	mathematical	—	TopCat.str AlexDisc.toTopCat CategoryTheory.Functor.obj Preord Preord.instCategory AlexDisc AlexDisc.category CategoryTheory.Equivalence.inverse alexDiscEquivPreord Topology.WithUpperSet.instTopologicalSpace Preord.carrier Preord.str	—	—
alexDiscEquivPreord_unitIso 📖	mathematical	—	CategoryTheory.Equivalence.unitIso AlexDisc Preord AlexDisc.category Preord.instCategory alexDiscEquivPreord CategoryTheory.NatIso.ofComponents CategoryTheory.Functor.id CategoryTheory.Functor.comp TopCat TopCat.instCategory CategoryTheory.forget₂ ContinuousMap TopCat.carrier AlexDisc.toTopCat TopCat.str ContinuousMap.instFunLike AlexDisc.concreteCategory TopCat.instConcreteCategoryContinuousMapCarrier AlexDisc.instHasForgetToTop topToPreord AlexDisc.of Topology.WithUpperSet Preord.carrier Topology.WithUpperSet.instTopologicalSpace Preord.str CategoryTheory.ConcreteCategory.ofHom Topology.WithUpperSet.map Preord.Hom.hom CategoryTheory.Functor.obj Homeomorph homeoWithUpperSetTopologyorderIso AlexDisc.is_alexandrovDiscrete	—	—

---

← Back to Index