Documentation Verification Report

Specialization

📁 Source: Mathlib/Topology/Specialization.lean

Statistics

Metric	Count
Definitions `Specialization`, `instPartialOrder`, `instPreorder`, `map`, `ofEquiv`, `rec`, `toEquiv`, `homeoWithUpperSetTopologyorderIso`, `orderIsoSpecializationWithUpperSetTopology`, `topToPreord`	10
Theorems `isOpen_toEquiv_preimage`, `isUpperSet_ofEquiv_preimage`, `map_comp`, `map_id`, `ofEquiv_inj`, `ofEquiv_specializes_ofEquiv`, `ofEquiv_symm`, `ofEquiv_toEquiv`, `toEquiv_inj`, `toEquiv_le_toEquiv`, `toEquiv_ofEquiv`, `toEquiv_symm`, `topToPreord_map`, `topToPreord_obj_coe`	14
Total	24

Specialization

Definitions

Name	Category	Theorems
`instPartialOrder` 📖	CompOp	—
`instPreorder` 📖	CompOp	8 math math: `isOpen_toEquiv_preimage`, `toEquiv_le_toEquiv`, `topToPreord_map`, `isUpperSet_ofEquiv_preimage`, `ofEquiv_specializes_ofEquiv`, `map_id`, `alexDiscEquivPreord_counitIso`, `map_comp`
`map` 📖	CompOp	3 math math: `topToPreord_map`, `map_id`, `map_comp`
`ofEquiv` 📖	CompOp	7 math math: `ofEquiv_toEquiv`, `ofEquiv_inj`, `isUpperSet_ofEquiv_preimage`, `toEquiv_symm`, `ofEquiv_specializes_ofEquiv`, `ofEquiv_symm`, `toEquiv_ofEquiv`
`rec` 📖	CompOp	—
`toEquiv` 📖	CompOp	7 math math: `ofEquiv_toEquiv`, `isOpen_toEquiv_preimage`, `toEquiv_inj`, `toEquiv_le_toEquiv`, `toEquiv_symm`, `ofEquiv_symm`, `toEquiv_ofEquiv`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isOpen_toEquiv_preimage` 📖	mathematical	—	`IsOpen` `Set.preimage` `Specialization` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toEquiv` `IsUpperSet` `Preorder.toLE` `instPreorder`	—	`isOpen_iff_forall_specializes` `forall_swap`
`isUpperSet_ofEquiv_preimage` 📖	mathematical	—	`IsUpperSet` `Specialization` `Preorder.toLE` `instPreorder` `Set.preimage` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofEquiv` `IsOpen`	—	`isOpen_toEquiv_preimage`
`map_comp` 📖	mathematical	—	`map` `ContinuousMap.comp` `OrderHom.comp` `Specialization` `instPreorder`	—	—
`map_id` 📖	mathematical	—	`map` `ContinuousMap.id` `OrderHom.id` `Specialization` `instPreorder`	—	—
`ofEquiv_inj` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Specialization` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofEquiv`	—	—
`ofEquiv_specializes_ofEquiv` 📖	mathematical	—	`Specializes` `DFunLike.coe` `Equiv` `Specialization` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofEquiv` `Preorder.toLE` `instPreorder`	—	—
`ofEquiv_symm` 📖	mathematical	—	`Equiv.symm` `Specialization` `ofEquiv` `toEquiv`	—	—
`ofEquiv_toEquiv` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Specialization` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofEquiv` `toEquiv`	—	—
`toEquiv_inj` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Specialization` `EquivLike.toFunLike` `Equiv.instEquivLike` `toEquiv`	—	—
`toEquiv_le_toEquiv` 📖	mathematical	—	`Specialization` `Preorder.toLE` `instPreorder` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toEquiv` `Specializes`	—	—
`toEquiv_ofEquiv` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Specialization` `EquivLike.toFunLike` `Equiv.instEquivLike` `toEquiv` `ofEquiv`	—	—
`toEquiv_symm` 📖	mathematical	—	`Equiv.symm` `Specialization` `toEquiv` `ofEquiv`	—	—

(root)

Definitions

Name	Category	Theorems
`Specialization` 📖	CompOp	15 math math: `Specialization.ofEquiv_toEquiv`, `Specialization.isOpen_toEquiv_preimage`, `Specialization.toEquiv_inj`, `Specialization.toEquiv_le_toEquiv`, `Specialization.ofEquiv_inj`, `topToPreord_map`, `Specialization.isUpperSet_ofEquiv_preimage`, `topToPreord_obj_coe`, `Specialization.toEquiv_symm`, `Specialization.ofEquiv_specializes_ofEquiv`, `Specialization.map_id`, `alexDiscEquivPreord_counitIso`, `Specialization.ofEquiv_symm`, `Specialization.map_comp`, `Specialization.toEquiv_ofEquiv`
`homeoWithUpperSetTopologyorderIso` 📖	CompOp	1 math math: `alexDiscEquivPreord_unitIso`
`orderIsoSpecializationWithUpperSetTopology` 📖	CompOp	1 math math: `alexDiscEquivPreord_counitIso`
`topToPreord` 📖	CompOp	5 math math: `alexDiscEquivPreord_unitIso`, `topToPreord_map`, `topToPreord_obj_coe`, `alexDiscEquivPreord_counitIso`, `alexDiscEquivPreord_functor`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`topToPreord_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `TopCat` `TopCat.instCategory` `Preord` `Preord.instCategory` `topToPreord` `Preord.ofHom` `Specialization` `TopCat.carrier` `Specialization.instPreorder` `TopCat.str` `Specialization.map` `TopCat.Hom.hom`	—	—
`topToPreord_obj_coe` 📖	mathematical	—	`Preord.carrier` `CategoryTheory.Functor.obj` `TopCat` `TopCat.instCategory` `Preord` `Preord.instCategory` `topToPreord` `Specialization` `TopCat.carrier`	—	—

---

← Back to Index