Documentation Verification Report

Birkhoff

📁 Source: Mathlib/Order/Birkhoff.lean

Statistics

Metric	Count
Definitions `birkhoffFinset`, `birkhoffSet`, `birkhoffFinset`, `birkhoffSet`, `infIrredUpperSet`, `supIrredLowerSet`, `infIrredUpperSet`, `lowerSetSupIrred`, `supIrredLowerSet`	9
Theorems `birkhoffFinset_injective`, `supIrred_Iic`, `supIrred_iff_of_finite`, `birkhoffFinset_inf`, `birkhoffFinset_sup`, `birkhoffSet_apply`, `birkhoffSet_inf`, `birkhoffSet_sup`, `coe_birkhoffFinset`, `infIrredUpperSet_apply`, `infIrredUpperSet_surjective`, `supIrredLowerSet_apply`, `supIrredLowerSet_surjective`, `infIrredUpperSet_apply`, `infIrredUpperSet_symm_apply`, `supIrredLowerSet_apply`, `supIrredLowerSet_symm_apply`, `infIrred_Ici`, `infIrred_iff_of_finite`, `exists_birkhoff_representation`	20
Total	29

LatticeHom

Definitions

Name	Category	Theorems
`birkhoffFinset` 📖	CompOp	1 math math: `birkhoffFinset_injective`
`birkhoffSet` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`birkhoffFinset_injective` 📖	mathematical	—	`Finset` `SupIrred` `Lattice.toSemilatticeSup` `DistribLattice.toLattice` `DFunLike.coe` `LatticeHom` `Finset.instLattice` `instFunLike` `birkhoffFinset`	—	`RelEmbedding.injective`

LowerSet

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`supIrred_Iic` 📖	mathematical	—	`SupIrred` `LowerSet` `Preorder.toLE` `PartialOrder.toPreorder` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `completeLattice` `Iic`	—	`Iic_ne_bot` `IsMin.eq_bot` `mem_Iic_iff` `le_refl` `LE.le.antisymm` `LE.le.trans_eq` `le_sup_left` `Iic_le` `le_sup_right`
`supIrred_iff_of_finite` 📖	mathematical	—	`SupIrred` `LowerSet` `Preorder.toLE` `PartialOrder.toPreorder` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `completeLattice` `Iic`	—	`Set.Finite.exists_maximal` `instIsTransLe` `Set.toFinite` `Subtype.finite` `coe_nonempty` `SupIrred.ne_bot` `erase_sup_Iic` `le_imp_eq_iff_le_imp_ge'` `LT.lt.ne` `erase_lt` `supIrred_Iic`

OrderEmbedding

Definitions

Name	Category	Theorems
`birkhoffFinset` 📖	CompOp	3 math math: `birkhoffFinset_inf`, `coe_birkhoffFinset`, `birkhoffFinset_sup`
`birkhoffSet` 📖	CompOp	4 math math: `coe_birkhoffFinset`, `birkhoffSet_inf`, `birkhoffSet_sup`, `birkhoffSet_apply`
`infIrredUpperSet` 📖	CompOp	2 math math: `infIrredUpperSet_surjective`, `infIrredUpperSet_apply`
`supIrredLowerSet` 📖	CompOp	2 math math: `supIrredLowerSet_apply`, `supIrredLowerSet_surjective`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`birkhoffFinset_inf` 📖	mathematical	—	`DFunLike.coe` `OrderEmbedding` `Finset` `SupIrred` `Lattice.toSemilatticeSup` `DistribLattice.toLattice` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `Finset.partialOrder` `instFunLikeOrderEmbedding` `birkhoffFinset` `SemilatticeInf.toMin` `Finset.instInter`	—	`birkhoffSet_inf` `OrderIso.coe_toOrderEmbedding` `Fintype.finsetEquivSet_symm_apply` `Set.toFinset_inter`
`birkhoffFinset_sup` 📖	mathematical	—	`DFunLike.coe` `OrderEmbedding` `Finset` `SupIrred` `Lattice.toSemilatticeSup` `DistribLattice.toLattice` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `Finset.partialOrder` `instFunLikeOrderEmbedding` `birkhoffFinset` `SemilatticeSup.toMax` `Finset.instUnion`	—	`birkhoffSet_sup` `OrderIso.coe_toOrderEmbedding` `Fintype.finsetEquivSet_symm_apply` `Set.toFinset_union`
`birkhoffSet_apply` 📖	mathematical	—	`DFunLike.coe` `OrderEmbedding` `Set` `SupIrred` `Lattice.toSemilatticeSup` `DistribLattice.toLattice` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `Set.instLE` `instFunLikeOrderEmbedding` `birkhoffSet` `SetLike.coe` `LowerSet` `LowerSet.instSetLike` `OrderIso` `LowerSet.instPartialOrder` `instFunLikeOrderIso` `OrderIso.lowerSetSupIrred`	—	`OrderBot.instSubsingleton` `bot_nonempty`
`birkhoffSet_inf` 📖	mathematical	—	`DFunLike.coe` `OrderEmbedding` `Set` `SupIrred` `Lattice.toSemilatticeSup` `DistribLattice.toLattice` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `Set.instLE` `instFunLikeOrderEmbedding` `birkhoffSet` `SemilatticeInf.toMin` `Set.instInter`	—	`InfHomClass.map_inf` `OrderIsoClass.toInfHomClass` `OrderIso.instOrderIsoClass` `inf_of_le_left` `IsEmpty.instSubsingleton` `Unique.instSubsingleton` `instIsEmptySubtype`
`birkhoffSet_sup` 📖	mathematical	—	`DFunLike.coe` `OrderEmbedding` `Set` `SupIrred` `Lattice.toSemilatticeSup` `DistribLattice.toLattice` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `Set.instLE` `instFunLikeOrderEmbedding` `birkhoffSet` `SemilatticeSup.toMax` `Set.instUnion`	—	`SupHomClass.map_sup` `LatticeHomClass.toSupHomClass` `OrderIsoClass.toLatticeHomClass` `OrderIso.instOrderIsoClass` `sup_of_le_left` `IsEmpty.instSubsingleton` `Unique.instSubsingleton` `instIsEmptySubtype`
`coe_birkhoffFinset` 📖	mathematical	—	`SetLike.coe` `Finset` `SupIrred` `Lattice.toSemilatticeSup` `DistribLattice.toLattice` `Finset.instSetLike` `DFunLike.coe` `OrderEmbedding` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `Finset.partialOrder` `instFunLikeOrderEmbedding` `birkhoffFinset` `Set` `Set.instLE` `birkhoffSet`	—	`OrderIso.coe_toOrderEmbedding` `Fintype.finsetEquivSet_symm_apply` `Set.coe_toFinset`
`infIrredUpperSet_apply` 📖	mathematical	—	`DFunLike.coe` `OrderEmbedding` `UpperSet` `Preorder.toLE` `PartialOrder.toPreorder` `InfIrred` `Lattice.toSemilatticeInf` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `UpperSet.completeLattice` `UpperSet.instPartialOrder` `instFunLikeOrderEmbedding` `infIrredUpperSet` `UpperSet.Ici` `UpperSet.infIrred_Ici`	—	—
`infIrredUpperSet_surjective` 📖	mathematical	—	`UpperSet` `Preorder.toLE` `PartialOrder.toPreorder` `InfIrred` `Lattice.toSemilatticeInf` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `UpperSet.completeLattice` `DFunLike.coe` `OrderEmbedding` `UpperSet.instPartialOrder` `instFunLikeOrderEmbedding` `infIrredUpperSet`	—	`UpperSet.infIrred_Ici`
`supIrredLowerSet_apply` 📖	mathematical	—	`DFunLike.coe` `OrderEmbedding` `LowerSet` `Preorder.toLE` `PartialOrder.toPreorder` `SupIrred` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `LowerSet.completeLattice` `LowerSet.instPartialOrder` `instFunLikeOrderEmbedding` `supIrredLowerSet` `LowerSet.Iic` `LowerSet.supIrred_Iic`	—	—
`supIrredLowerSet_surjective` 📖	mathematical	—	`LowerSet` `Preorder.toLE` `PartialOrder.toPreorder` `SupIrred` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `LowerSet.completeLattice` `DFunLike.coe` `OrderEmbedding` `LowerSet.instPartialOrder` `instFunLikeOrderEmbedding` `supIrredLowerSet`	—	`LowerSet.supIrred_Iic`

OrderIso

Definitions

Name	Category	Theorems
`infIrredUpperSet` 📖	CompOp	2 math math: `infIrredUpperSet_symm_apply`, `infIrredUpperSet_apply`
`lowerSetSupIrred` 📖	CompOp	1 math math: `OrderEmbedding.birkhoffSet_apply`
`supIrredLowerSet` 📖	CompOp	2 math math: `supIrredLowerSet_symm_apply`, `supIrredLowerSet_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`infIrredUpperSet_apply` 📖	mathematical	—	`DFunLike.coe` `OrderIso` `UpperSet` `Preorder.toLE` `PartialOrder.toPreorder` `InfIrred` `Lattice.toSemilatticeInf` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `UpperSet.completeLattice` `UpperSet.instPartialOrder` `instFunLikeOrderIso` `infIrredUpperSet` `UpperSet.Ici` `UpperSet.infIrred_Ici`	—	—
`infIrredUpperSet_symm_apply` 📖	mathematical	—	`DFunLike.coe` `OrderIso` `UpperSet` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `InfIrred` `Lattice.toSemilatticeInf` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `UpperSet.completeLattice` `UpperSet.instPartialOrder` `instFunLikeOrderIso` `symm` `infIrredUpperSet` `Finset.inf` `Set.toFinset` `SetLike.coe` `UpperSet.instSetLike`	—	`UpperSet.infIrred_iff_of_finite` `nonempty_fintype` `Set.toFinset_Ici` `Finset.inf_Ici`
`supIrredLowerSet_apply` 📖	mathematical	—	`DFunLike.coe` `OrderIso` `LowerSet` `Preorder.toLE` `PartialOrder.toPreorder` `SupIrred` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `LowerSet.completeLattice` `LowerSet.instPartialOrder` `instFunLikeOrderIso` `supIrredLowerSet` `LowerSet.Iic` `LowerSet.supIrred_Iic`	—	—
`supIrredLowerSet_symm_apply` 📖	mathematical	—	`DFunLike.coe` `OrderIso` `LowerSet` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `SupIrred` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `LowerSet.completeLattice` `LowerSet.instPartialOrder` `instFunLikeOrderIso` `symm` `supIrredLowerSet` `Finset.sup` `Set.toFinset` `SetLike.coe` `LowerSet.instSetLike`	—	`LowerSet.supIrred_iff_of_finite` `nonempty_fintype` `Set.toFinset_Iic` `Finset.sup_Iic`

UpperSet

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`infIrred_Ici` 📖	mathematical	—	`InfIrred` `UpperSet` `Preorder.toLE` `PartialOrder.toPreorder` `Lattice.toSemilatticeInf` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `completeLattice` `Ici`	—	`Ici_ne_top` `IsMax.eq_top` `mem_Ici_iff` `le_refl` `le_antisymm` `le_Ici` `LE.le.trans` `Eq.ge` `inf_le_left` `inf_le_right`
`infIrred_iff_of_finite` 📖	mathematical	—	`InfIrred` `UpperSet` `Preorder.toLE` `PartialOrder.toPreorder` `Lattice.toSemilatticeInf` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `completeLattice` `Ici`	—	`Set.Finite.exists_minimal` `instIsTransLe` `Set.toFinite` `Subtype.finite` `coe_nonempty` `InfIrred.ne_top` `erase_inf_Ici` `le_imp_eq_iff_le_imp_ge` `LT.lt.ne'` `lt_erase` `infIrred_Ici`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_birkhoff_representation` 📖	mathematical	—	`Finset` `DFunLike.coe` `LatticeHom` `DistribLattice.toLattice` `Finset.instLattice` `LatticeHom.instFunLike`	—	`nonempty_fintype` `LatticeHom.birkhoffFinset_injective`

---

← Back to Index