Documentation Verification Report

LawsonTopology

📁 Source: Mathlib/Topology/Order/LawsonTopology.lean

Statistics

Metric	Count
Definitions `IsLawson`, `lawsonBasis`, `WithLawson`, `homeomorph`, `instInhabited`, `instPreorder`, `instTopologicalSpace`, `ofLawson`, `rec`, `toLawson`, `lawson`	11
Theorems `isTopologicalBasis`, `toT1Space`, `topology_eq_lawson`, `instIsLawson`, `instNonempty`, `isClosed_preimage_ofLawson`, `isOpen_def`, `isOpen_preimage_ofLawson`, `ofLawson_inj`, `ofLawson_toLawson`, `of_Lawson_symm_eq`, `toLawson_inj`, `toLawson_ofLawson`, `to_Lawson_symm_eq`, `isLawson_le_isScott`, `lawsonClosed_iff_dirSupClosed_of_isLowerSet`, `lawsonClosed_iff_scottClosed_of_isLowerSet`, `lawsonClosed_of_lowerClosed`, `lawsonClosed_of_scottClosed`, `lawsonOpen_iff_scottOpen_of_isUpperSet`, `lawsonOpen_iff_scottOpen_of_isUpperSet'`, `lawson_le_lower`, `lawson_le_scott`, `scottHausdorff_le_isLawson`, `scottHausdorff_le_lawson`	25
Total	36

Topology

Definitions

Name	Category	Theorems
`IsLawson` 📖	CompData	1 math math: `WithLawson.instIsLawson`
`WithLawson` 📖	CompOp	14 math math: `lawsonClosed_of_lowerClosed`, `WithLawson.ofLawson_toLawson`, `WithLawson.isOpen_preimage_ofLawson`, `WithLawson.toLawson_inj`, `WithLawson.isOpen_def`, `WithLawson.instNonempty`, `WithLawson.ofLawson_inj`, `WithLawson.to_Lawson_symm_eq`, `lawsonClosed_of_scottClosed`, `WithLawson.isClosed_preimage_ofLawson`, `WithLawson.instIsLawson`, `lawsonOpen_iff_scottOpen_of_isUpperSet`, `WithLawson.of_Lawson_symm_eq`, `WithLawson.toLawson_ofLawson`
`lawson` 📖	CompOp	7 math math: `lawson_le_scott`, `WithLawson.isOpen_preimage_ofLawson`, `WithLawson.isOpen_def`, `scottHausdorff_le_lawson`, `WithLawson.isClosed_preimage_ofLawson`, `lawson_le_lower`, `IsLawson.topology_eq_lawson`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isLawson_le_isScott` 📖	mathematical	—	`TopologicalSpace` `Preorder.toLE` `PartialOrder.toPreorder` `TopologicalSpace.instPartialOrder`	—	`IsScott.topology_eq` `IsLawson.topology_eq_lawson` `inf_le_right`
`lawsonClosed_iff_dirSupClosed_of_isLowerSet` 📖	mathematical	`IsLowerSet` `Preorder.toLE`	`IsClosed` `DirSupClosed`	—	`lawsonClosed_iff_scottClosed_of_isLowerSet` `IsScott.isClosed_iff_isLowerSet_and_dirSupClosed`
`lawsonClosed_iff_scottClosed_of_isLowerSet` 📖	mathematical	`IsLowerSet` `Preorder.toLE`	`IsClosed`	—	`isOpen_compl_iff` `lawsonOpen_iff_scottOpen_of_isUpperSet'` `isUpperSet_compl`
`lawsonClosed_of_lowerClosed` 📖	mathematical	—	`IsClosed` `WithLawson` `WithLawson.instTopologicalSpace` `Set.preimage` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `WithLawson.ofLawson`	—	`IsClosed.mono` `lawson_le_lower`
`lawsonClosed_of_scottClosed` 📖	mathematical	—	`IsClosed` `WithLawson` `WithLawson.instTopologicalSpace` `Set.preimage` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `WithLawson.ofLawson`	—	`IsClosed.mono` `lawson_le_scott`
`lawsonOpen_iff_scottOpen_of_isUpperSet` 📖	mathematical	`IsUpperSet` `Preorder.toLE`	`IsOpen` `WithLawson` `WithLawson.instTopologicalSpace` `Set.preimage` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `WithLawson.ofLawson` `WithScott` `WithScott.instTopologicalSpace` `WithScott.ofScott`	—	`IsScott.isOpen_iff_isUpperSet_and_scottHausdorff_open` `WithScott.instIsScottUnivSet` `scottHausdorff_le_lawson` `lawson_le_scott`
`lawsonOpen_iff_scottOpen_of_isUpperSet'` 📖	mathematical	`IsUpperSet` `Preorder.toLE`	`IsOpen`	—	`IsLawson.topology_eq_lawson` `IsScott.topology_eq` `lawsonOpen_iff_scottOpen_of_isUpperSet`
`lawson_le_lower` 📖	mathematical	—	`TopologicalSpace` `Preorder.toLE` `PartialOrder.toPreorder` `TopologicalSpace.instPartialOrder` `lawson` `lower`	—	`inf_le_left`
`lawson_le_scott` 📖	mathematical	—	`TopologicalSpace` `Preorder.toLE` `PartialOrder.toPreorder` `TopologicalSpace.instPartialOrder` `lawson` `scott` `Set.univ` `Set`	—	`inf_le_right`
`scottHausdorff_le_isLawson` 📖	mathematical	—	`TopologicalSpace` `Preorder.toLE` `PartialOrder.toPreorder` `TopologicalSpace.instPartialOrder` `scottHausdorff` `Set.univ` `Set`	—	`IsLawson.topology_eq_lawson` `scottHausdorff_le_lawson`
`scottHausdorff_le_lawson` 📖	mathematical	—	`TopologicalSpace` `Preorder.toLE` `PartialOrder.toPreorder` `TopologicalSpace.instPartialOrder` `scottHausdorff` `Set.univ` `Set` `lawson`	—	`le_inf` `scottHausdorff_le_lower` `scottHausdorff_le_scott`

Topology.IsLawson

Definitions

Name	Category	Theorems
`lawsonBasis` 📖	CompOp	1 math math: `isTopologicalBasis`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isTopologicalBasis` 📖	mathematical	—	`TopologicalSpace.IsTopologicalBasis` `lawsonBasis`	—	`lawsonBasis.eq_1` `Set.image2.eq_1` `Topology.IsLower.lowerBasis.eq_1` `Set.diff_eq_compl_inter` `topology_eq_lawson` `Topology.lawson.eq_1` `Topology.IsInducing.eq_induced` `Homeomorph.isInducing` `TopologicalSpace.IsTopologicalBasis.inf_induced` `Topology.IsLower.isTopologicalBasis` `Topology.instIsLowerWithLower` `TopologicalSpace.isTopologicalBasis_opens`
`toT1Space` 📖	mathematical	—	`T1Space`	—	`topology_eq_lawson` `Set.OrdConnected.upperClosure_inter_lowerClosure` `Set.ordConnected_singleton` `Topology.WithLawson.isClosed_preimage_ofLawson` `IsClosed.inter` `Topology.lawsonClosed_of_lowerClosed` `Topology.IsLower.isClosed_upperClosure` `Topology.instIsLowerWithLower` `Set.finite_singleton` `lowerClosure_singleton` `LowerSet.coe_Iic` `Topology.lawsonClosed_of_scottClosed` `isClosed_Iic` `Topology.IsScott.instClosedIicTopologyOfUnivSet` `Topology.WithScott.instIsScottUnivSet`
`topology_eq_lawson` 📖	mathematical	—	`Topology.lawson`	—	—

Topology.WithLawson

Definitions

Name	Category	Theorems
`homeomorph` 📖	CompOp	—
`instInhabited` 📖	CompOp	—
`instPreorder` 📖	CompOp	1 math math: `instIsLawson`
`instTopologicalSpace` 📖	CompOp	7 math math: `Topology.lawsonClosed_of_lowerClosed`, `isOpen_preimage_ofLawson`, `isOpen_def`, `Topology.lawsonClosed_of_scottClosed`, `isClosed_preimage_ofLawson`, `instIsLawson`, `Topology.lawsonOpen_iff_scottOpen_of_isUpperSet`
`ofLawson` 📖	CompOp	10 math math: `Topology.lawsonClosed_of_lowerClosed`, `ofLawson_toLawson`, `isOpen_preimage_ofLawson`, `ofLawson_inj`, `to_Lawson_symm_eq`, `Topology.lawsonClosed_of_scottClosed`, `isClosed_preimage_ofLawson`, `Topology.lawsonOpen_iff_scottOpen_of_isUpperSet`, `of_Lawson_symm_eq`, `toLawson_ofLawson`
`rec` 📖	CompOp	—
`toLawson` 📖	CompOp	6 math math: `ofLawson_toLawson`, `toLawson_inj`, `isOpen_def`, `to_Lawson_symm_eq`, `of_Lawson_symm_eq`, `toLawson_ofLawson`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsLawson` 📖	mathematical	—	`Topology.IsLawson` `Topology.WithLawson` `instPreorder` `instTopologicalSpace`	—	—
`instNonempty` 📖	mathematical	—	`Topology.WithLawson`	—	—
`isClosed_preimage_ofLawson` 📖	mathematical	—	`IsClosed` `Topology.WithLawson` `instTopologicalSpace` `Set.preimage` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofLawson` `Topology.lawson`	—	—
`isOpen_def` 📖	mathematical	—	`IsOpen` `Topology.WithLawson` `instTopologicalSpace` `TopologicalSpace.IsOpen` `Topology.lawson` `Set.preimage` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toLawson`	—	—
`isOpen_preimage_ofLawson` 📖	mathematical	—	`IsOpen` `Topology.WithLawson` `instTopologicalSpace` `Set.preimage` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofLawson` `TopologicalSpace.IsOpen` `Topology.lawson`	—	—
`ofLawson_inj` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Topology.WithLawson` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofLawson`	—	—
`ofLawson_toLawson` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Topology.WithLawson` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofLawson` `toLawson`	—	—
`of_Lawson_symm_eq` 📖	mathematical	—	`Equiv.symm` `Topology.WithLawson` `ofLawson` `toLawson`	—	—
`toLawson_inj` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Topology.WithLawson` `EquivLike.toFunLike` `Equiv.instEquivLike` `toLawson`	—	—
`toLawson_ofLawson` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Topology.WithLawson` `EquivLike.toFunLike` `Equiv.instEquivLike` `toLawson` `ofLawson`	—	—
`to_Lawson_symm_eq` 📖	mathematical	—	`Equiv.symm` `Topology.WithLawson` `toLawson` `ofLawson`	—	—

---

← Back to Index