Documentation Verification Report

Ordered

📁 Source: Mathlib/Topology/ContinuousMap/Ordered.lean

Statistics

Metric	Count
Definitions `IccExtend`, `inf`, `instLatticeOfTopologicalLattice`, `partialOrder`, `semilatticeInf`, `semilatticeSup`, `sup`	7
Theorems `coe_IccExtend`, `coe_inf`, `coe_inf'`, `coe_sup`, `coe_sup'`, `inf'_apply`, `inf_apply`, `le_def`, `lt_def`, `sup'_apply`, `sup_apply`	11
Total	18

ContinuousMap

Definitions

Name	Category	Theorems
`IccExtend` 📖	CompOp	1 math math: `coe_IccExtend`
`inf` 📖	CompOp	4 math math: `inf_apply`, `inf_mem_subalgebra_closure`, `inf_mem_closed_subalgebra`, `coe_inf`
`instLatticeOfTopologicalLattice` 📖	CompOp	5 math math: `abs_mem_subalgebra_closure`, `abs_apply`, `coe_mabs`, `mabs_apply`, `coe_abs`
`partialOrder` 📖	CompOp	10 math math: `le_def`, `cfcHom_nonneg_iff`, `PartitionOfUnity.nonneg'`, `cfcHom_le_iff`, `lt_def`, `instStarOrderedRingOfContinuousSqrt`, `instIsOrderedAddMonoid`, `BumpCovering.nonneg'`, `instIsOrderedMonoid`, `BumpCovering.le_one'`
`semilatticeInf` 📖	CompOp	2 math math: `coe_inf'`, `inf'_apply`
`semilatticeSup` 📖	CompOp	2 math math: `coe_sup'`, `sup'_apply`
`sup` 📖	CompOp	4 math math: `sup_apply`, `sup_mem_closed_subalgebra`, `sup_mem_subalgebra_closure`, `coe_sup`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_IccExtend` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`DFunLike.coe` `ContinuousMap` `instFunLike` `IccExtend` `Set.IccExtend` `Set.Elem` `Set.Icc` `instTopologicalSpaceSubtype` `Set` `Set.instMembership`	—	—
`coe_inf` 📖	mathematical	—	`DFunLike.coe` `ContinuousMap` `instFunLike` `inf` `Pi.instMinForall_mathlib` `SemilatticeInf.toMin`	—	—
`coe_inf'` 📖	mathematical	`Finset.Nonempty`	`DFunLike.coe` `ContinuousMap` `instFunLike` `Finset.inf'` `semilatticeInf` `Pi.instSemilatticeInf`	—	`inf'_apply` `Finset.inf'_apply`
`coe_sup` 📖	mathematical	—	`DFunLike.coe` `ContinuousMap` `instFunLike` `sup` `Pi.instMaxForall_mathlib` `SemilatticeSup.toMax`	—	—
`coe_sup'` 📖	mathematical	`Finset.Nonempty`	`DFunLike.coe` `ContinuousMap` `instFunLike` `Finset.sup'` `semilatticeSup` `Pi.instSemilatticeSup`	—	`sup'_apply` `Finset.sup'_apply`
`inf'_apply` 📖	mathematical	`Finset.Nonempty`	`DFunLike.coe` `ContinuousMap` `instFunLike` `Finset.inf'` `semilatticeInf`	—	`Finset.comp_inf'_eq_inf'_comp`
`inf_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousMap` `instFunLike` `inf` `SemilatticeInf.toMin`	—	—
`le_def` 📖	mathematical	—	`ContinuousMap` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `DFunLike.coe` `instFunLike`	—	`Pi.le_def`
`lt_def` 📖	mathematical	—	`ContinuousMap` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `Preorder.toLE` `DFunLike.coe` `instFunLike`	—	`Pi.lt_def`
`sup'_apply` 📖	mathematical	`Finset.Nonempty`	`DFunLike.coe` `ContinuousMap` `instFunLike` `Finset.sup'` `semilatticeSup`	—	`Finset.comp_sup'_eq_sup'_comp`
`sup_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousMap` `instFunLike` `sup` `SemilatticeSup.toMax`	—	—

---

← Back to Index