Documentation Verification Report

DirSupClosed

📁 Source: Mathlib/Order/DirSupClosed.lean

Statistics

Metric	Count
Definitions `DirSupClosed`, `DirSupInacc`, `DirSupInaccOn`	3
Theorems `compl`, `inter`, `of_compl`, `compl`, `dirSupInaccOn`, `of_compl`, `union`, `mono`, `dirSupInacc`, `dirSupClosed`, `dirSupClosed_Iic`, `dirSupClosed_compl`, `dirSupClosed_iff_forall_sSup`, `dirSupInaccOn_univ`, `dirSupInacc_compl`, `dirSupInacc_iff_forall_sSup`	16
Total	19

DirSupClosed

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`compl` 📖	mathematical	`DirSupClosed`	`DirSupInacc` `Compl.compl` `Set` `Set.instCompl`	—	`dirSupInacc_compl`
`inter` 📖	mathematical	`DirSupClosed`	`DirSupClosed` `Set` `Set.instInter`	—	`HasSubset.Subset.trans` `Set.instIsTransSubset` `Set.inter_subset_left` `Set.inter_subset_right`
`of_compl` 📖	mathematical	`DirSupClosed` `Compl.compl` `Set` `Set.instCompl`	`DirSupInacc`	—	`dirSupClosed_compl`

DirSupInacc

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`compl` 📖	mathematical	`DirSupInacc`	`DirSupClosed` `Compl.compl` `Set` `Set.instCompl`	—	`dirSupClosed_compl`
`dirSupInaccOn` 📖	mathematical	`DirSupInacc`	`DirSupInaccOn`	—	—
`of_compl` 📖	mathematical	`DirSupInacc` `Compl.compl` `Set` `Set.instCompl`	`DirSupClosed`	—	`dirSupInacc_compl`
`union` 📖	mathematical	`DirSupInacc`	`DirSupInacc` `Set` `Set.instUnion`	—	`dirSupClosed_compl` `Set.compl_union` `DirSupClosed.inter` `compl`

DirSupInaccOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mono` 📖	mathematical	`Set` `Set.instHasSubset` `DirSupInaccOn`	`DirSupInaccOn`	—	—

IsLowerSet

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dirSupInacc` 📖	mathematical	`IsLowerSet` `Preorder.toLE`	`DirSupInacc`	—	`DirSupClosed.of_compl` `IsUpperSet.dirSupClosed` `compl`

IsUpperSet

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dirSupClosed` 📖	mathematical	`IsUpperSet` `Preorder.toLE`	`DirSupClosed`	—	—

(root)

Definitions

Name	Category	Theorems
`DirSupClosed` 📖	MathDef	13 math math: `dirSupClosed_iff_forall_sSup`, `Topology.IsScott.isClosed_iff_isLowerSet_and_dirSupClosed`, `IsUpperSet.dirSupClosed`, `Topology.IsScottHausdorff.isClosed_iff_dirSupClosed`, `dirSupClosed_Iic`, `dirSupInacc_compl`, `DirSupClosed.inter`, `DirSupInacc.of_compl`, `Topology.lawsonClosed_iff_dirSupClosed_of_isLowerSet`, `dirSupClosed_compl`, `Topology.IsScottHausdorff.dirSupClosed_of_isClosed`, `DirSupInacc.compl`, `Topology.IsScott.dirSupClosed_of_isClosed`
`DirSupInacc` 📖	MathDef	9 math math: `DirSupClosed.of_compl`, `DirSupClosed.compl`, `dirSupInacc_compl`, `DirSupInacc.union`, `Topology.IsScottHausdorff.isOpen_iff_dirSupInacc`, `dirSupInaccOn_univ`, `dirSupClosed_compl`, `IsLowerSet.dirSupInacc`, `dirSupInacc_iff_forall_sSup`
`DirSupInaccOn` 📖	MathDef	5 math math: `Topology.IsScottHausdorff.dirSupInaccOn_of_isOpen`, `DirSupInaccOn.mono`, `dirSupInaccOn_univ`, `Topology.IsScott.isOpen_iff_isUpperSet_and_dirSupInaccOn`, `DirSupInacc.dirSupInaccOn`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dirSupClosed_Iic` 📖	mathematical	—	`DirSupClosed` `Set.Iic`	—	`isLUB_le_iff`
`dirSupClosed_compl` 📖	mathematical	—	`DirSupClosed` `Compl.compl` `Set` `Set.instCompl` `DirSupInacc`	—	`dirSupInacc_compl` `compl_compl`
`dirSupClosed_iff_forall_sSup` 📖	mathematical	—	`DirSupClosed` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `Set` `Set.instMembership` `SupSet.sSup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup`	—	—
`dirSupInaccOn_univ` 📖	mathematical	—	`DirSupInaccOn` `Set.univ` `Set` `DirSupInacc`	—	—
`dirSupInacc_compl` 📖	mathematical	—	`DirSupInacc` `Compl.compl` `Set` `Set.instCompl` `DirSupClosed`	—	—
`dirSupInacc_iff_forall_sSup` 📖	mathematical	—	`DirSupInacc` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `Set.Nonempty` `Set` `Set.instInter`	—	—

---

← Back to Index