Documentation Verification Report

UpperLowerSetTopology

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

Statistics

Metric	Count
Definitions `IsLowerSet`, `WithLowerSetHomeomorph`, `IsUpperSet`, `WithUpperSetHomeomorph`, `WithLowerSet`, `instInhabited`, `instPreorder`, `instTopologicalSpace`, `map`, `ofLowerSet`, `ofLowerSetOrderIso`, `rec`, `toLowerSet`, `toLowerSetOrderIso`, `WithUpperSet`, `instInhabited`, `instPreorder`, `instTopologicalSpace`, `map`, `ofUpperSet`, `ofUpperSetOrderIso`, `rec`, `toDualHomeomorph`, `toUpperSet`, `toUpperSetOrderIso`, `lowerSet`, `upperSet`	27
Theorems `instIsLowerSet`, `instIsUpperSet`, `closure_eq_upperClosure`, `closure_singleton`, `isClosed_iff_isUpper`, `isOpen_iff_isLowerSet`, `lowerSet_le_lower`, `monotone_iff_continuous`, `monotone_to_lowerTopology_continuous`, `nhdsKer_eq_lowerClosure`, `nhdsKer_singleton`, `nhdsSet_eq_principal_lowerClosure`, `nhds_eq_principal_Iic`, `specializes_iff_le`, `toAlexandrovDiscrete`, `topology_eq`, `topology_eq_lowerSetTopology`, `closure_eq_lowerClosure`, `closure_singleton`, `instProp`, `isClosed_iff_isLower`, `isOpen_iff_isUpperSet`, `monotone_iff_continuous`, `monotone_to_upperTopology_continuous`, `nhdsKer_eq_upperClosure`, `nhdsKer_singleton`, `nhdsSet_eq_principal_upperClosure`, `nhds_eq_principal_Ici`, `specializes_iff_le`, `toAlexandrovDiscrete`, `topology_eq`, `topology_eq_upperSetTopology`, `upperSet_le_upper`, `instNonempty`, `isLowerSet_toLowerSet_preimage`, `isOpen_ofLowerSet_preimage`, `map_comp`, `map_id`, `ofLowerSet_inj`, `ofLowerSet_le_iff`, `ofLowerSet_le_ofLowerSet`, `ofLowerSet_symm`, `ofLowerSet_toLowerSet`, `toLowerSet_inj`, `toLowerSet_le_iff`, `toLowerSet_ofLowerSet`, `toLowerSet_specializes_toLowerSet`, `toLowerSet_symm`, `instNonempty`, `isOpen_ofUpperSet_preimage`, `isUpperSet_toUpperSet_preimage`, `map_comp`, `map_id`, `ofUpperSet_inj`, `ofUpperSet_le_iff`, `ofUpperSet_le_ofUpperSet`, `ofUpperSet_symm`, `ofUpperSet_toUpperSet`, `toUpperSet_inj`, `toUpperSet_le_iff`, `toUpperSet_ofUpperSet`, `toUpperSet_specializes_toUpperSet`, `toUpperSet_symm`, `instIsLowerSet`, `instIsLowerSetWithLowerSet`, `instIsUpperSet`, `instIsUpperSetWithUpperSet`, `isLowerSet_iff_nhds`, `isLowerSet_orderDual`, `isUpperSet_iff_nhds`, `isUpperSet_orderDual`	71
Total	98

OrderDual

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsLowerSet` 📖	mathematical	—	`Topology.IsLowerSet` `OrderDual` `instTopologicalSpace` `instPreorder`	—	`TopologicalSpace.ext` `Topology.IsUpperSet.topology_eq`
`instIsUpperSet` 📖	mathematical	—	`Topology.IsUpperSet` `OrderDual` `instTopologicalSpace` `instPreorder`	—	`TopologicalSpace.ext` `Topology.IsLowerSet.topology_eq`

Topology

Definitions

Name	Category	Theorems
`IsLowerSet` 📖	CompData	6 math math: `instIsLowerSetWithLowerSet`, `OrderDual.instIsLowerSet`, `isUpperSet_orderDual`, `instIsLowerSet`, `isLowerSet_iff_nhds`, `isLowerSet_orderDual`
`IsUpperSet` 📖	CompData	7 math math: `isUpperSet_orderDual`, `instIsUpperSetWithUpperSet`, `isUpperSet_iff_nhds`, `OrderDual.instIsUpperSet`, `isLowerSet_orderDual`, `instIsUpperSet`, `IsUpperSet.instProp`
`WithLowerSet` 📖	CompOp	16 math math: `WithLowerSet.ofLowerSet_inj`, `instIsLowerSetWithLowerSet`, `WithLowerSet.map_comp`, `WithLowerSet.isLowerSet_toLowerSet_preimage`, `WithLowerSet.toLowerSet_ofLowerSet`, `WithLowerSet.toLowerSet_symm`, `WithLowerSet.toLowerSet_inj`, `WithLowerSet.ofLowerSet_le_iff`, `WithLowerSet.toLowerSet_le_iff`, `WithLowerSet.instNonempty`, `WithLowerSet.map_id`, `WithLowerSet.isOpen_ofLowerSet_preimage`, `WithLowerSet.ofLowerSet_le_ofLowerSet`, `WithLowerSet.ofLowerSet_toLowerSet`, `WithLowerSet.toLowerSet_specializes_toLowerSet`, `WithLowerSet.ofLowerSet_symm`
`WithUpperSet` 📖	CompOp	20 math math: `WithUpperSet.toUpperSet_inj`, `alexDiscEquivPreord_inverse_obj_carrier`, `WithUpperSet.toUpperSet_symm`, `WithUpperSet.toUpperSet_specializes_toUpperSet`, `alexDiscEquivPreord_inverse_map`, `WithUpperSet.instNonempty`, `WithUpperSet.isUpperSet_toUpperSet_preimage`, `WithUpperSet.ofUpperSet_le_iff`, `instIsUpperSetWithUpperSet`, `WithUpperSet.toUpperSet_le_iff`, `WithUpperSet.ofUpperSet_toUpperSet`, `WithUpperSet.ofUpperSet_le_ofUpperSet`, `alexDiscEquivPreord_unitIso`, `WithUpperSet.ofUpperSet_inj`, `WithUpperSet.toUpperSet_ofUpperSet`, `WithUpperSet.map_comp`, `WithUpperSet.ofUpperSet_symm`, `alexDiscEquivPreord_counitIso`, `WithUpperSet.isOpen_ofUpperSet_preimage`, `WithUpperSet.map_id`
`lowerSet` 📖	CompOp	3 math math: `IsLowerSet.topology_eq`, `instIsLowerSet`, `IsLowerSet.topology_eq_lowerSetTopology`
`upperSet` 📖	CompOp	4 math math: `IsUpperSet.topology_eq`, `IsUpperSet.topology_eq_upperSetTopology`, `upperSet_le_scott`, `instIsUpperSet`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsLowerSet` 📖	mathematical	—	`IsLowerSet` `lowerSet`	—	—
`instIsLowerSetWithLowerSet` 📖	mathematical	—	`IsLowerSet` `WithLowerSet` `WithLowerSet.instTopologicalSpace` `WithLowerSet.instPreorder`	—	—
`instIsUpperSet` 📖	mathematical	—	`IsUpperSet` `upperSet`	—	—
`instIsUpperSetWithUpperSet` 📖	mathematical	—	`IsUpperSet` `WithUpperSet` `WithUpperSet.instTopologicalSpace` `WithUpperSet.instPreorder`	—	—
`isLowerSet_iff_nhds` 📖	mathematical	—	`IsLowerSet` `nhds` `Filter.principal` `Set.Iic`	—	`IsLowerSet.nhds_eq_principal_Iic` `instIsLowerSet`
`isLowerSet_orderDual` 📖	mathematical	—	`IsLowerSet` `OrderDual` `OrderDual.instTopologicalSpace` `OrderDual.instPreorder` `IsUpperSet`	—	`isUpperSet_orderDual`
`isUpperSet_iff_nhds` 📖	mathematical	—	`IsUpperSet` `nhds` `Filter.principal` `Set.Ici`	—	`IsUpperSet.nhds_eq_principal_Ici` `instIsUpperSet`
`isUpperSet_orderDual` 📖	mathematical	—	`IsUpperSet` `OrderDual` `OrderDual.instTopologicalSpace` `OrderDual.instPreorder` `IsLowerSet`	—	`OrderDual.instIsLowerSet` `OrderDual.instIsUpperSet`

Topology.IsLowerSet

Definitions

Name	Category	Theorems
`WithLowerSetHomeomorph` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`closure_eq_upperClosure` 📖	mathematical	—	`closure` `SetLike.coe` `UpperSet` `Preorder.toLE` `UpperSet.instSetLike` `upperClosure`	—	`Topology.IsUpperSet.closure_eq_lowerClosure` `OrderDual.instIsUpperSet`
`closure_singleton` 📖	mathematical	—	`closure` `Set` `Set.instSingletonSet` `Set.Ici`	—	`closure_eq_upperClosure` `upperClosure_singleton`
`isClosed_iff_isUpper` 📖	mathematical	—	`IsClosed` `IsUpperSet` `Preorder.toLE`	—	`isOpen_compl_iff` `isOpen_iff_isLowerSet` `isUpperSet_compl` `compl_compl`
`isOpen_iff_isLowerSet` 📖	mathematical	—	`IsOpen` `IsLowerSet` `Preorder.toLE`	—	`topology_eq`
`lowerSet_le_lower` 📖	mathematical	—	`TopologicalSpace` `Preorder.toLE` `PartialOrder.toPreorder` `TopologicalSpace.instPartialOrder`	—	`isOpen_iff_isLowerSet` `Topology.IsLower.isLowerSet_of_isOpen`
`monotone_iff_continuous` 📖	mathematical	—	`Monotone` `Continuous`	—	`monotone_dual_iff` `Topology.IsUpperSet.monotone_iff_continuous` `OrderDual.instIsUpperSet`
`monotone_to_lowerTopology_continuous` 📖	mathematical	`Monotone`	`Continuous`	—	`Topology.IsUpperSet.monotone_to_upperTopology_continuous` `OrderDual.instIsUpperSet` `OrderDual.instIsUpper` `Monotone.dual`
`nhdsKer_eq_lowerClosure` 📖	mathematical	—	`nhdsKer` `SetLike.coe` `LowerSet` `Preorder.toLE` `LowerSet.instSetLike` `lowerClosure`	—	`Set.ext`
`nhdsKer_singleton` 📖	mathematical	—	`nhdsKer` `Set` `Set.instSingletonSet` `Set.Iic`	—	`nhdsKer_eq_lowerClosure` `lowerClosure_singleton` `LowerSet.coe_Iic`
`nhdsSet_eq_principal_lowerClosure` 📖	mathematical	—	`nhdsSet` `Filter.principal` `SetLike.coe` `LowerSet` `Preorder.toLE` `LowerSet.instSetLike` `lowerClosure`	—	`principal_nhdsKer` `toAlexandrovDiscrete` `nhdsKer_eq_lowerClosure`
`nhds_eq_principal_Iic` 📖	mathematical	—	`nhds` `Filter.principal` `Set.Iic`	—	`principal_nhdsKer_singleton` `toAlexandrovDiscrete` `nhdsKer_singleton`
`specializes_iff_le` 📖	mathematical	—	`Specializes` `Preorder.toLE`	—	`closure_singleton`
`toAlexandrovDiscrete` 📖	mathematical	—	`AlexandrovDiscrete`	—	`Topology.IsUpperSet.toAlexandrovDiscrete` `OrderDual.instIsUpperSet`
`topology_eq` 📖	mathematical	—	`Topology.lowerSet`	—	`topology_eq_lowerSetTopology`
`topology_eq_lowerSetTopology` 📖	mathematical	—	`Topology.lowerSet`	—	—

Topology.IsUpperSet

Definitions

Name	Category	Theorems
`WithUpperSetHomeomorph` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`closure_eq_lowerClosure` 📖	mathematical	—	`closure` `SetLike.coe` `LowerSet` `Preorder.toLE` `LowerSet.instSetLike` `lowerClosure`	—	`subset_antisymm_iff` `Set.instReflSubset` `Set.instAntisymmSubset` `closure_minimal` `subset_lowerClosure` `isClosed_iff_isLower` `LowerSet.lower` `lowerClosure_min` `subset_closure` `isClosed_closure`
`closure_singleton` 📖	mathematical	—	`closure` `Set` `Set.instSingletonSet` `Set.Iic`	—	`closure_eq_lowerClosure` `lowerClosure_singleton`
`instProp` 📖	mathematical	—	`Topology.IsUpperSet` `sierpinskiSpace` `PartialOrder.toPreorder` `Prop.partialOrder`	—	`nhds_true` `Set.Ici_True` `Filter.principal_singleton` `nhds_false` `Set.Ici_False` `Filter.principal_univ`
`isClosed_iff_isLower` 📖	mathematical	—	`IsClosed` `IsLowerSet` `Preorder.toLE`	—	`isOpen_compl_iff` `isOpen_iff_isUpperSet` `isLowerSet_compl` `compl_compl`
`isOpen_iff_isUpperSet` 📖	mathematical	—	`IsOpen` `IsUpperSet` `Preorder.toLE`	—	`topology_eq`
`monotone_iff_continuous` 📖	mathematical	—	`Monotone` `Continuous`	—	`IsUpperSet.preimage` `Set.mem_Iic` `closure_singleton` `Continuous.closure_preimage_subset` `Set.mem_of_mem_of_subset` `closure_mono` `Set.singleton_subset_iff` `Set.mem_preimage` `Set.mem_singleton_iff`
`monotone_to_upperTopology_continuous` 📖	mathematical	`Monotone`	`Continuous`	—	`IsUpperSet.preimage` `Topology.IsUpper.isUpperSet_of_isOpen`
`nhdsKer_eq_upperClosure` 📖	mathematical	—	`nhdsKer` `SetLike.coe` `UpperSet` `Preorder.toLE` `UpperSet.instSetLike` `upperClosure`	—	`Set.ext`
`nhdsKer_singleton` 📖	mathematical	—	`nhdsKer` `Set` `Set.instSingletonSet` `Set.Ici`	—	`nhdsKer_eq_upperClosure` `upperClosure_singleton` `UpperSet.coe_Ici`
`nhdsSet_eq_principal_upperClosure` 📖	mathematical	—	`nhdsSet` `Filter.principal` `SetLike.coe` `UpperSet` `Preorder.toLE` `UpperSet.instSetLike` `upperClosure`	—	`principal_nhdsKer` `toAlexandrovDiscrete` `nhdsKer_eq_upperClosure`
`nhds_eq_principal_Ici` 📖	mathematical	—	`nhds` `Filter.principal` `Set.Ici`	—	`principal_nhdsKer_singleton` `toAlexandrovDiscrete` `nhdsKer_singleton`
`specializes_iff_le` 📖	mathematical	—	`Specializes` `Preorder.toLE`	—	`closure_singleton`
`toAlexandrovDiscrete` 📖	mathematical	—	`AlexandrovDiscrete`	—	`isUpperSet_sInter`
`topology_eq` 📖	mathematical	—	`Topology.upperSet`	—	`topology_eq_upperSetTopology`
`topology_eq_upperSetTopology` 📖	mathematical	—	`Topology.upperSet`	—	—
`upperSet_le_upper` 📖	mathematical	—	`TopologicalSpace` `Preorder.toLE` `PartialOrder.toPreorder` `TopologicalSpace.instPartialOrder`	—	`isOpen_iff_isUpperSet` `Topology.IsUpper.isUpperSet_of_isOpen`

Topology.WithLowerSet

Definitions

Name	Category	Theorems
`instInhabited` 📖	CompOp	—
`instPreorder` 📖	CompOp	3 math math: `Topology.instIsLowerSetWithLowerSet`, `ofLowerSet_le_iff`, `toLowerSet_le_iff`
`instTopologicalSpace` 📖	CompOp	7 math math: `Topology.instIsLowerSetWithLowerSet`, `map_comp`, `isLowerSet_toLowerSet_preimage`, `map_id`, `isOpen_ofLowerSet_preimage`, `ofLowerSet_le_ofLowerSet`, `toLowerSet_specializes_toLowerSet`
`map` 📖	CompOp	2 math math: `map_comp`, `map_id`
`ofLowerSet` 📖	CompOp	8 math math: `ofLowerSet_inj`, `toLowerSet_ofLowerSet`, `toLowerSet_symm`, `ofLowerSet_le_iff`, `isOpen_ofLowerSet_preimage`, `ofLowerSet_le_ofLowerSet`, `ofLowerSet_toLowerSet`, `ofLowerSet_symm`
`ofLowerSetOrderIso` 📖	CompOp	—
`rec` 📖	CompOp	—
`toLowerSet` 📖	CompOp	8 math math: `isLowerSet_toLowerSet_preimage`, `toLowerSet_ofLowerSet`, `toLowerSet_symm`, `toLowerSet_inj`, `toLowerSet_le_iff`, `ofLowerSet_toLowerSet`, `toLowerSet_specializes_toLowerSet`, `ofLowerSet_symm`
`toLowerSetOrderIso` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instNonempty` 📖	mathematical	—	`Topology.WithLowerSet`	—	—
`isLowerSet_toLowerSet_preimage` 📖	mathematical	—	`IsLowerSet` `Preorder.toLE` `Set.preimage` `Topology.WithLowerSet` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toLowerSet` `IsOpen` `instTopologicalSpace`	—	—
`isOpen_ofLowerSet_preimage` 📖	mathematical	—	`IsOpen` `Topology.WithLowerSet` `instTopologicalSpace` `Set.preimage` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofLowerSet` `IsLowerSet` `Preorder.toLE`	—	`isLowerSet_toLowerSet_preimage`
`map_comp` 📖	mathematical	—	`map` `OrderHom.comp` `ContinuousMap.comp` `Topology.WithLowerSet` `instTopologicalSpace`	—	—
`map_id` 📖	mathematical	—	`map` `OrderHom.id` `ContinuousMap.id` `Topology.WithLowerSet` `instTopologicalSpace`	—	—
`ofLowerSet_inj` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Topology.WithLowerSet` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofLowerSet`	—	—
`ofLowerSet_le_iff` 📖	mathematical	—	`Preorder.toLE` `DFunLike.coe` `Equiv` `Topology.WithLowerSet` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofLowerSet` `instPreorder`	—	—
`ofLowerSet_le_ofLowerSet` 📖	mathematical	—	`Preorder.toLE` `DFunLike.coe` `Equiv` `Topology.WithLowerSet` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofLowerSet` `Specializes` `instTopologicalSpace`	—	`toLowerSet_specializes_toLowerSet`
`ofLowerSet_symm` 📖	mathematical	—	`Equiv.symm` `Topology.WithLowerSet` `ofLowerSet` `toLowerSet`	—	—
`ofLowerSet_toLowerSet` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Topology.WithLowerSet` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofLowerSet` `toLowerSet`	—	—
`toLowerSet_inj` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Topology.WithLowerSet` `EquivLike.toFunLike` `Equiv.instEquivLike` `toLowerSet`	—	—
`toLowerSet_le_iff` 📖	mathematical	—	`Topology.WithLowerSet` `Preorder.toLE` `instPreorder` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toLowerSet`	—	—
`toLowerSet_ofLowerSet` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Topology.WithLowerSet` `EquivLike.toFunLike` `Equiv.instEquivLike` `toLowerSet` `ofLowerSet`	—	—
`toLowerSet_specializes_toLowerSet` 📖	mathematical	—	`Specializes` `Topology.WithLowerSet` `instTopologicalSpace` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toLowerSet` `Preorder.toLE`	—	`Topology.IsLowerSet.closure_singleton` `Topology.instIsLowerSetWithLowerSet`
`toLowerSet_symm` 📖	mathematical	—	`Equiv.symm` `Topology.WithLowerSet` `toLowerSet` `ofLowerSet`	—	—

Topology.WithUpperSet

Definitions

Name	Category	Theorems
`instInhabited` 📖	CompOp	—
`instPreorder` 📖	CompOp	3 math math: `ofUpperSet_le_iff`, `Topology.instIsUpperSetWithUpperSet`, `toUpperSet_le_iff`
`instTopologicalSpace` 📖	CompOp	11 math math: `alexDiscEquivPreord_inverse_obj_str`, `toUpperSet_specializes_toUpperSet`, `alexDiscEquivPreord_inverse_map`, `isUpperSet_toUpperSet_preimage`, `Topology.instIsUpperSetWithUpperSet`, `ofUpperSet_le_ofUpperSet`, `alexDiscEquivPreord_unitIso`, `map_comp`, `alexDiscEquivPreord_counitIso`, `isOpen_ofUpperSet_preimage`, `map_id`
`map` 📖	CompOp	5 math math: `alexDiscEquivPreord_inverse_map`, `alexDiscEquivPreord_unitIso`, `map_comp`, `alexDiscEquivPreord_counitIso`, `map_id`
`ofUpperSet` 📖	CompOp	8 math math: `toUpperSet_symm`, `ofUpperSet_le_iff`, `ofUpperSet_toUpperSet`, `ofUpperSet_le_ofUpperSet`, `ofUpperSet_inj`, `toUpperSet_ofUpperSet`, `ofUpperSet_symm`, `isOpen_ofUpperSet_preimage`
`ofUpperSetOrderIso` 📖	CompOp	—
`rec` 📖	CompOp	—
`toDualHomeomorph` 📖	CompOp	—
`toUpperSet` 📖	CompOp	8 math math: `toUpperSet_inj`, `toUpperSet_symm`, `toUpperSet_specializes_toUpperSet`, `isUpperSet_toUpperSet_preimage`, `toUpperSet_le_iff`, `ofUpperSet_toUpperSet`, `toUpperSet_ofUpperSet`, `ofUpperSet_symm`
`toUpperSetOrderIso` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instNonempty` 📖	mathematical	—	`Topology.WithUpperSet`	—	—
`isOpen_ofUpperSet_preimage` 📖	mathematical	—	`IsOpen` `Topology.WithUpperSet` `instTopologicalSpace` `Set.preimage` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofUpperSet` `IsUpperSet` `Preorder.toLE`	—	`isUpperSet_toUpperSet_preimage`
`isUpperSet_toUpperSet_preimage` 📖	mathematical	—	`IsUpperSet` `Preorder.toLE` `Set.preimage` `Topology.WithUpperSet` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toUpperSet` `IsOpen` `instTopologicalSpace`	—	—
`map_comp` 📖	mathematical	—	`map` `OrderHom.comp` `ContinuousMap.comp` `Topology.WithUpperSet` `instTopologicalSpace`	—	—
`map_id` 📖	mathematical	—	`map` `OrderHom.id` `ContinuousMap.id` `Topology.WithUpperSet` `instTopologicalSpace`	—	—
`ofUpperSet_inj` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Topology.WithUpperSet` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofUpperSet`	—	—
`ofUpperSet_le_iff` 📖	mathematical	—	`Preorder.toLE` `DFunLike.coe` `Equiv` `Topology.WithUpperSet` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofUpperSet` `instPreorder`	—	—
`ofUpperSet_le_ofUpperSet` 📖	mathematical	—	`Preorder.toLE` `DFunLike.coe` `Equiv` `Topology.WithUpperSet` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofUpperSet` `Specializes` `instTopologicalSpace`	—	`toUpperSet_specializes_toUpperSet`
`ofUpperSet_symm` 📖	mathematical	—	`Equiv.symm` `Topology.WithUpperSet` `ofUpperSet` `toUpperSet`	—	—
`ofUpperSet_toUpperSet` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Topology.WithUpperSet` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofUpperSet` `toUpperSet`	—	—
`toUpperSet_inj` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Topology.WithUpperSet` `EquivLike.toFunLike` `Equiv.instEquivLike` `toUpperSet`	—	—
`toUpperSet_le_iff` 📖	mathematical	—	`Topology.WithUpperSet` `Preorder.toLE` `instPreorder` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toUpperSet`	—	—
`toUpperSet_ofUpperSet` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Topology.WithUpperSet` `EquivLike.toFunLike` `Equiv.instEquivLike` `toUpperSet` `ofUpperSet`	—	—
`toUpperSet_specializes_toUpperSet` 📖	mathematical	—	`Specializes` `Topology.WithUpperSet` `instTopologicalSpace` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toUpperSet` `Preorder.toLE`	—	`Topology.IsUpperSet.closure_singleton` `Topology.instIsUpperSetWithUpperSet`
`toUpperSet_symm` 📖	mathematical	—	`Equiv.symm` `Topology.WithUpperSet` `toUpperSet` `ofUpperSet`	—	—

---

← Back to Index