Documentation Verification Report

LatticeIntervals

📁 Source: Mathlib/Order/LatticeIntervals.lean

Statistics

Metric	Count
Definitions `instBoundedOrderElemOfFactLe`, `instOrderBotElemOfFactLe`, `instOrderTopElemOfFactLe`, `lattice`, `semilatticeInf`, `semilatticeSup`, `boundedOrder`, `distribLattice`, `lattice`, `orderBot`, `orderTop`, `semilatticeInf`, `semilatticeSup`, `orderBot`, `semilatticeInf`, `instBoundedOrderElemOfOrderBot`, `instLatticeElem`, `orderBot`, `orderTop`, `semilatticeInf`, `semilatticeSup`, `semilatticeInf`, `orderTop`, `semilatticeSup`, `semilatticeSup`	25
Theorems `codisjoint_iff`, `coe_bot`, `coe_inf`, `coe_sup`, `coe_top`, `disjoint_iff`, `isCompl_iff`, `codisjoint_iff`, `coe_bot`, `coe_inf`, `coe_sup`, `coe_top`, `disjoint_iff`, `isCompl_iff`, `coe_bot`, `coe_inf`, `disjoint_iff`, `codisjoint_iff`, `coe_bot`, `coe_inf`, `coe_sup`, `coe_top`, `complementedLattice_iff`, `disjoint_iff`, `eq_top_iff`, `isCompl_iff`, `coe_inf`, `codisjoint_iff`, `coe_sup`, `coe_top`, `coe_sup`	31
Total	56

Set.Icc

Definitions

Name	Category	Theorems
`instBoundedOrderElemOfFactLe` 📖	CompOp	2 math math: `isCompl_iff`, `IsModularLattice.complementedLattice_Icc`
`instOrderBotElemOfFactLe` 📖	CompOp	9 math math: `Icc_isBoundaryPoint_bot`, `ContinuousMap.concatCM_left`, `disjoint_iff`, `IccLeftChart_extend_bot`, `coe_bot`, `ContinuousMap.concatCM_right`, `boundary_Icc`, `boundary_product`, `IccLeftChart_extend_bot_mem_frontier`
`instOrderTopElemOfFactLe` 📖	CompOp	9 math math: `ContinuousMap.concatCM_left`, `codisjoint_iff`, `IccRightChart_extend_top_mem_frontier`, `ContinuousMap.concatCM_right`, `coe_top`, `IccRightChart_extend_top`, `boundary_Icc`, `boundary_product`, `Icc_isBoundaryPoint_top`
`lattice` 📖	CompOp	4 math math: `Path.range_subpathAux`, `unitInterval.volume_uIcc`, `Path.range_subpath`, `IsModularLattice.complementedLattice_Icc`
`semilatticeInf` 📖	CompOp	1 math math: `coe_inf`
`semilatticeSup` 📖	CompOp	1 math math: `coe_sup`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`codisjoint_iff` 📖	mathematical	—	`Codisjoint` `Set.Elem` `Set.Icc` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Subtype.partialOrder` `Set` `Set.instMembership` `instOrderTopElemOfFactLe` `SemilatticeSup.toMax`	—	—
`coe_bot` 📖	mathematical	—	`Set` `Set.instMembership` `Set.Icc` `Bot.bot` `Set.Elem` `OrderBot.toBot` `Preorder.toLE` `instOrderBotElemOfFactLe`	—	—
`coe_inf` 📖	mathematical	—	`Set` `Set.instMembership` `Set.Icc` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Set.Elem` `SemilatticeInf.toMin` `semilatticeInf`	—	—
`coe_sup` 📖	mathematical	—	`Set` `Set.instMembership` `Set.Icc` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Set.Elem` `SemilatticeSup.toMax` `semilatticeSup`	—	—
`coe_top` 📖	mathematical	—	`Set` `Set.instMembership` `Set.Icc` `Top.top` `Set.Elem` `OrderTop.toTop` `Preorder.toLE` `instOrderTopElemOfFactLe`	—	—
`disjoint_iff` 📖	mathematical	—	`Disjoint` `Set.Elem` `Set.Icc` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Subtype.partialOrder` `Set` `Set.instMembership` `instOrderBotElemOfFactLe` `SemilatticeInf.toMin`	—	—
`isCompl_iff` 📖	mathematical	—	`IsCompl` `Set.Elem` `Set.Icc` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `Subtype.partialOrder` `Set` `Set.instMembership` `instBoundedOrderElemOfFactLe` `SemilatticeInf.toMin` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup`	—	`isCompl_iff` `disjoint_iff` `codisjoint_iff`

Set.Ici

Definitions

Name	Category	Theorems
`boundedOrder` 📖	CompOp	3 math math: `IsModularLattice.complementedLattice_Ici`, `isCompl_iff`, `Set.isSimpleOrder_Ici_iff_isCoatom`
`distribLattice` 📖	CompOp	—
`lattice` 📖	CompOp	2 math math: `IsModularLattice.complementedLattice_Ici`, `IsModularLattice.isModularLattice_Ici`
`orderBot` 📖	CompOp	8 math math: `coe_bot`, `isAtom_iff`, `CategoryTheory.TransfiniteCompositionOfShape.ici_F`, `covBy_iff_atom_Ici`, `disjoint_iff`, `CategoryTheory.TransfiniteCompositionOfShape.ici_isoBot`, `CategoryTheory.TransfiniteCompositionOfShape.ici_isColimit`, `CategoryTheory.TransfiniteCompositionOfShape.ici_incl`
`orderTop` 📖	CompOp	5 math math: `isCoatomic_iff_forall_isCoatomic_Ici`, `codisjoint_iff`, `IsCoatomic.Set.Ici.isCoatomic`, `coe_top`, `IsCoatom.Ici`
`semilatticeInf` 📖	CompOp	1 math math: `coe_inf`
`semilatticeSup` 📖	CompOp	1 math math: `coe_sup`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`codisjoint_iff` 📖	mathematical	—	`Codisjoint` `Set.Elem` `Set.Ici` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Subtype.partialOrder` `Set` `Set.instMembership` `orderTop`	—	—
`coe_bot` 📖	mathematical	—	`Set` `Set.instMembership` `Set.Ici` `Bot.bot` `Set.Elem` `OrderBot.toBot` `Preorder.toLE` `orderBot`	—	—
`coe_inf` 📖	mathematical	—	`Set` `Set.instMembership` `Set.Ici` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Set.Elem` `SemilatticeInf.toMin` `semilatticeInf`	—	—
`coe_sup` 📖	mathematical	—	`Set` `Set.instMembership` `Set.Ici` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Set.Elem` `SemilatticeSup.toMax` `semilatticeSup`	—	—
`coe_top` 📖	mathematical	—	`Set` `Set.instMembership` `Set.Ici` `Top.top` `Set.Elem` `OrderTop.toTop` `Preorder.toLE` `orderTop`	—	—
`disjoint_iff` 📖	mathematical	—	`Disjoint` `Set.Elem` `Set.Ici` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Subtype.partialOrder` `Set` `Set.instMembership` `orderBot` `SemilatticeInf.toMin`	—	—
`isCompl_iff` 📖	mathematical	—	`IsCompl` `Set.Elem` `Set.Ici` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `Subtype.partialOrder` `Set` `Set.instMembership` `boundedOrder` `SemilatticeInf.toMin` `Codisjoint`	—	`isCompl_iff` `disjoint_iff` `codisjoint_iff`

Set.Ico

Definitions

Name	Category	Theorems
`orderBot` 📖	CompOp	2 math math: `coe_bot`, `disjoint_iff`
`semilatticeInf` 📖	CompOp	1 math math: `coe_inf`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_bot` 📖	mathematical	—	`Set` `Set.instMembership` `Set.Ico` `PartialOrder.toPreorder` `Bot.bot` `Set.Elem` `OrderBot.toBot` `Preorder.toLE` `orderBot`	—	—
`coe_inf` 📖	mathematical	—	`Set` `Set.instMembership` `Set.Ico` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Set.Elem` `SemilatticeInf.toMin` `semilatticeInf`	—	—
`disjoint_iff` 📖	mathematical	—	`Disjoint` `Set.Elem` `Set.Ico` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Subtype.partialOrder` `Set` `Set.instMembership` `orderBot` `SemilatticeInf.toMin`	—	—

Set.Iic

Definitions

Name	Category	Theorems
`instBoundedOrderElemOfOrderBot` 📖	CompOp	5 math math: `isCompl_inf_inf_of_isCompl_of_le`, `complementedLattice_iff`, `Set.isSimpleOrder_Iic_iff_isAtom`, `isCompl_iff`, `IsModularLattice.complementedLattice_Iic`
`instLatticeElem` 📖	CompOp	3 math math: `complementedLattice_iff`, `IsModularLattice.isModularLattice_Iic`, `IsModularLattice.complementedLattice_Iic`
`orderBot` 📖	CompOp	9 math math: `CategoryTheory.TransfiniteCompositionOfShape.iic_isoBot`, `isAtomic_iff_forall_isAtomic_Iic`, `CategoryTheory.TransfiniteCompositionOfShape.iic_isColimit`, `IsAtomic.Set.Iic.isAtomic`, `disjoint_iff`, `IsAtom.Iic`, `CategoryTheory.TransfiniteCompositionOfShape.iic_F`, `CategoryTheory.TransfiniteCompositionOfShape.iic_incl_app`, `coe_bot`
`orderTop` 📖	CompOp	7 math math: `covBy_iff_coatom_Iic`, `CategoryTheory.TransfiniteCompositionOfShape.iic_isColimit`, `CompleteLattice.Iic_coatomic_of_compact_element`, `codisjoint_iff`, `coe_top`, `isCoatom_iff`, `eq_top_iff`
`semilatticeInf` 📖	CompOp	1 math math: `coe_inf`
`semilatticeSup` 📖	CompOp	1 math math: `coe_sup`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`codisjoint_iff` 📖	mathematical	—	`Codisjoint` `Set.Elem` `Set.Iic` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Subtype.partialOrder` `Set` `Set.instMembership` `orderTop` `SemilatticeSup.toMax`	—	`eq_top_iff`
`coe_bot` 📖	mathematical	—	`Set` `Set.instMembership` `Set.Iic` `Bot.bot` `Set.Elem` `OrderBot.toBot` `Preorder.toLE` `orderBot`	—	—
`coe_inf` 📖	mathematical	—	`Set` `Set.instMembership` `Set.Iic` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Set.Elem` `SemilatticeInf.toMin` `semilatticeInf`	—	—
`coe_sup` 📖	mathematical	—	`Set` `Set.instMembership` `Set.Iic` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Set.Elem` `SemilatticeSup.toMax` `semilatticeSup`	—	—
`coe_top` 📖	mathematical	—	`Set` `Set.instMembership` `Set.Iic` `Top.top` `Set.Elem` `OrderTop.toTop` `Preorder.toLE` `orderTop`	—	—
`complementedLattice_iff` 📖	mathematical	—	`ComplementedLattice` `Set.Elem` `Set.Iic` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `instLatticeElem` `instBoundedOrderElemOfOrderBot` `Preorder.toLE` `SemilatticeInf.toMin` `Bot.bot` `OrderBot.toBot` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup`	—	—
`disjoint_iff` 📖	mathematical	—	`Disjoint` `Set.Elem` `Set.Iic` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Subtype.partialOrder` `Set` `Set.instMembership` `orderBot`	—	—
`eq_top_iff` 📖	mathematical	—	`Top.top` `Set.Elem` `Set.Iic` `OrderTop.toTop` `Preorder.toLE` `Set` `Set.instMembership` `orderTop`	—	—
`isCompl_iff` 📖	mathematical	—	`IsCompl` `Set.Elem` `Set.Iic` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `Subtype.partialOrder` `Set` `Set.instMembership` `instBoundedOrderElemOfOrderBot` `Disjoint` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup`	—	`isCompl_iff` `disjoint_iff` `codisjoint_iff`

Set.Iio

Definitions

Name	Category	Theorems
`semilatticeInf` 📖	CompOp	1 math math: `coe_inf`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_inf` 📖	mathematical	—	`Set` `Set.instMembership` `Set.Iio` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Set.Elem` `SemilatticeInf.toMin` `semilatticeInf`	—	—

Set.Ioc

Definitions

Name	Category	Theorems
`orderTop` 📖	CompOp	2 math math: `coe_top`, `codisjoint_iff`
`semilatticeSup` 📖	CompOp	1 math math: `coe_sup`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`codisjoint_iff` 📖	mathematical	—	`Codisjoint` `Set.Elem` `Set.Ioc` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Subtype.partialOrder` `Set` `Set.instMembership` `orderTop` `SemilatticeSup.toMax`	—	—
`coe_sup` 📖	mathematical	—	`Set` `Set.instMembership` `Set.Ioc` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Set.Elem` `SemilatticeSup.toMax` `semilatticeSup`	—	—
`coe_top` 📖	mathematical	—	`Set` `Set.instMembership` `Set.Ioc` `PartialOrder.toPreorder` `Top.top` `Set.Elem` `OrderTop.toTop` `Preorder.toLE` `orderTop`	—	—

Set.Ioi

Definitions

Name	Category	Theorems
`semilatticeSup` 📖	CompOp	1 math math: `coe_sup`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_sup` 📖	mathematical	—	`Set` `Set.instMembership` `Set.Ioi` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Set.Elem` `SemilatticeSup.toMax` `semilatticeSup`	—	—

---

← Back to Index