Documentation Verification Report

Order

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

Statistics

Metric	Count
Definitions `ClopenUpperSet`, `instBot`, `instBoundedOrder`, `instInhabited`, `instLattice`, `instMax`, `instMin`, `instPartialOrder`, `instSetLike`, `instTop`, `toClopens`, `toUpperSet`	12
Theorems `coe_bot`, `coe_inf`, `coe_mk`, `coe_sup`, `coe_toUpperSet`, `coe_top`, `ext`, `ext_iff`, `isClopen`, `upper`, `upper'`	11
Total	23

ClopenUpperSet

Definitions

Name	Category	Theorems
`instBot` 📖	CompOp	1 math math: `coe_bot`
`instBoundedOrder` 📖	CompOp	—
`instInhabited` 📖	CompOp	—
`instLattice` 📖	CompOp	—
`instMax` 📖	CompOp	1 math math: `coe_sup`
`instMin` 📖	CompOp	1 math math: `coe_inf`
`instPartialOrder` 📖	CompOp	—
`instSetLike` 📖	CompOp	9 math math: `coe_toUpperSet`, `coe_bot`, `coe_sup`, `isClopen`, `coe_mk`, `upper`, `ext_iff`, `coe_inf`, `coe_top`
`instTop` 📖	CompOp	1 math math: `coe_top`
`toClopens` 📖	CompOp	1 math math: `upper'`
`toUpperSet` 📖	CompOp	1 math math: `coe_toUpperSet`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_bot` 📖	mathematical	—	`SetLike.coe` `ClopenUpperSet` `instSetLike` `Bot.bot` `instBot` `Set` `Set.instEmptyCollection`	—	—
`coe_inf` 📖	mathematical	—	`SetLike.coe` `ClopenUpperSet` `instSetLike` `instMin` `Set` `Set.instInter`	—	—
`coe_mk` 📖	mathematical	`IsUpperSet` `TopologicalSpace.Clopens.carrier`	`SetLike.coe` `ClopenUpperSet` `instSetLike` `TopologicalSpace.Clopens` `TopologicalSpace.Clopens.instSetLike`	—	—
`coe_sup` 📖	mathematical	—	`SetLike.coe` `ClopenUpperSet` `instSetLike` `instMax` `Set` `Set.instUnion`	—	—
`coe_toUpperSet` 📖	mathematical	—	`SetLike.coe` `UpperSet` `UpperSet.instSetLike` `toUpperSet` `ClopenUpperSet` `instSetLike`	—	—
`coe_top` 📖	mathematical	—	`SetLike.coe` `ClopenUpperSet` `instSetLike` `Top.top` `instTop` `Set.univ`	—	—
`ext` 📖	—	`SetLike.coe` `ClopenUpperSet` `instSetLike`	—	—	`SetLike.ext'`
`ext_iff` 📖	mathematical	—	`SetLike.coe` `ClopenUpperSet` `instSetLike`	—	`ext`
`isClopen` 📖	mathematical	—	`IsClopen` `SetLike.coe` `ClopenUpperSet` `instSetLike`	—	`TopologicalSpace.Clopens.isClopen'`
`upper` 📖	mathematical	—	`IsUpperSet` `SetLike.coe` `ClopenUpperSet` `instSetLike`	—	`upper'`
`upper'` 📖	mathematical	—	`IsUpperSet` `TopologicalSpace.Clopens.carrier` `toClopens`	—	—

(root)

Definitions

Name	Category	Theorems
`ClopenUpperSet` 📖	CompData	9 math math: `ClopenUpperSet.coe_toUpperSet`, `ClopenUpperSet.coe_bot`, `ClopenUpperSet.coe_sup`, `ClopenUpperSet.isClopen`, `ClopenUpperSet.coe_mk`, `ClopenUpperSet.upper`, `ClopenUpperSet.ext_iff`, `ClopenUpperSet.coe_inf`, `ClopenUpperSet.coe_top`

---

← Back to Index