Documentation Verification Report

Lex

📁 Source: Mathlib/Order/Hom/Lex.lean

Statistics

Metric	Count
Definitions `sumLexIicIoi`, `sumLexIioIci`, `prodLexAssoc`, `prodLexCongr`, `prodUnique`, `sumLexProdLexDistrib`, `uniqueProd`, `sumLexComplLeft`, `sumLexComplRight`	9
Theorems `sumLexIicIoi_apply_inl`, `sumLexIicIoi_apply_inr`, `sumLexIicIoi_symm_apply_Iic`, `sumLexIicIoi_symm_apply_Ioi`, `sumLexIicIoi_symm_apply_of_le`, `sumLexIicIoi_symm_apply_of_lt`, `sumLexIioIci_apply_inl`, `sumLexIioIci_apply_inr`, `sumLexIioIci_symm_apply_Ici`, `sumLexIioIci_symm_apply_Iio`, `sumLexIioIci_symm_apply_of_ge`, `sumLexIioIci_symm_apply_of_lt`, `prodLexAssoc_apply`, `prodLexAssoc_symm_apply`, `prodLexCongr_apply`, `prodUnique_apply`, `sumLexProdLexDistrib_apply`, `sumLexProdLexDistrib_symm_apply`, `uniqueProd_apply`, `sumLexComplLeft_apply`, `sumLexComplLeft_symm_apply`, `sumLexComplRight_apply`, `sumLexComplRight_symm_apply`	23
Total	32

OrderIso

Definitions

Name	Category	Theorems
`sumLexIicIoi` 📖	CompOp	6 math math: `sumLexIicIoi_symm_apply_of_lt`, `sumLexIicIoi_symm_apply_of_le`, `sumLexIicIoi_symm_apply_Iic`, `sumLexIicIoi_symm_apply_Ioi`, `sumLexIicIoi_apply_inr`, `sumLexIicIoi_apply_inl`
`sumLexIioIci` 📖	CompOp	6 math math: `sumLexIioIci_symm_apply_Ici`, `sumLexIioIci_symm_apply_Iio`, `sumLexIioIci_symm_apply_of_ge`, `sumLexIioIci_apply_inl`, `sumLexIioIci_apply_inr`, `sumLexIioIci_symm_apply_of_lt`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`sumLexIicIoi_apply_inl` 📖	mathematical	—	`DFunLike.coe` `OrderIso` `Lex` `Set.Elem` `Set.Iic` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set.Ioi` `Sum.Lex.LE` `Preorder.toLE` `Set` `Set.instMembership` `instFunLikeOrderIso` `sumLexIicIoi` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toLex`	—	—
`sumLexIicIoi_apply_inr` 📖	mathematical	—	`DFunLike.coe` `OrderIso` `Lex` `Set.Elem` `Set.Iic` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set.Ioi` `Sum.Lex.LE` `Preorder.toLE` `Set` `Set.instMembership` `instFunLikeOrderIso` `sumLexIicIoi` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toLex`	—	—
`sumLexIicIoi_symm_apply_Iic` 📖	mathematical	—	`DFunLike.coe` `OrderIso` `Lex` `Set.Elem` `Set.Iic` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set.Ioi` `Preorder.toLE` `Sum.Lex.LE` `Set` `Set.instMembership` `instFunLikeOrderIso` `symm` `sumLexIicIoi`	—	`sumLexIicIoi_symm_apply_of_le`
`sumLexIicIoi_symm_apply_Ioi` 📖	mathematical	—	`DFunLike.coe` `OrderIso` `Lex` `Set.Elem` `Set.Iic` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set.Ioi` `Preorder.toLE` `Sum.Lex.LE` `Set` `Set.instMembership` `instFunLikeOrderIso` `symm` `sumLexIicIoi`	—	`sumLexIicIoi_symm_apply_of_lt`
`sumLexIicIoi_symm_apply_of_le` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`DFunLike.coe` `OrderIso` `Lex` `Set.Elem` `Set.Iic` `Set.Ioi` `Sum.Lex.LE` `Set` `Set.instMembership` `instFunLikeOrderIso` `symm` `sumLexIicIoi` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toLex`	—	`symm_apply_eq` `sumLexIicIoi_apply_inl`
`sumLexIicIoi_symm_apply_of_lt` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`DFunLike.coe` `OrderIso` `Lex` `Set.Elem` `Set.Iic` `Set.Ioi` `Preorder.toLE` `Sum.Lex.LE` `Set` `Set.instMembership` `instFunLikeOrderIso` `symm` `sumLexIicIoi` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toLex`	—	`symm_apply_eq` `sumLexIicIoi_apply_inr`
`sumLexIioIci_apply_inl` 📖	mathematical	—	`DFunLike.coe` `OrderIso` `Lex` `Set.Elem` `Set.Iio` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set.Ici` `Sum.Lex.LE` `Preorder.toLE` `Set` `Set.instMembership` `instFunLikeOrderIso` `sumLexIioIci` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toLex`	—	—
`sumLexIioIci_apply_inr` 📖	mathematical	—	`DFunLike.coe` `OrderIso` `Lex` `Set.Elem` `Set.Iio` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set.Ici` `Sum.Lex.LE` `Preorder.toLE` `Set` `Set.instMembership` `instFunLikeOrderIso` `sumLexIioIci` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toLex`	—	—
`sumLexIioIci_symm_apply_Ici` 📖	mathematical	—	`DFunLike.coe` `OrderIso` `Lex` `Set.Elem` `Set.Iio` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set.Ici` `Preorder.toLE` `Sum.Lex.LE` `Set` `Set.instMembership` `instFunLikeOrderIso` `symm` `sumLexIioIci` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toLex`	—	`sumLexIioIci_symm_apply_of_ge`
`sumLexIioIci_symm_apply_Iio` 📖	mathematical	—	`DFunLike.coe` `OrderIso` `Lex` `Set.Elem` `Set.Iio` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set.Ici` `Preorder.toLE` `Sum.Lex.LE` `Set` `Set.instMembership` `instFunLikeOrderIso` `symm` `sumLexIioIci` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toLex`	—	`sumLexIioIci_symm_apply_of_lt`
`sumLexIioIci_symm_apply_of_ge` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`DFunLike.coe` `OrderIso` `Lex` `Set.Elem` `Set.Iio` `Set.Ici` `Sum.Lex.LE` `Set` `Set.instMembership` `instFunLikeOrderIso` `symm` `sumLexIioIci` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toLex`	—	`symm_apply_eq` `sumLexIioIci_apply_inr`
`sumLexIioIci_symm_apply_of_lt` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`DFunLike.coe` `OrderIso` `Lex` `Set.Elem` `Set.Iio` `Set.Ici` `Preorder.toLE` `Sum.Lex.LE` `Set` `Set.instMembership` `instFunLikeOrderIso` `symm` `sumLexIioIci` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toLex`	—	`symm_apply_eq` `sumLexIioIci_apply_inl`

Prod.Lex

Definitions

Name	Category	Theorems
`prodLexAssoc` 📖	CompOp	2 math math: `prodLexAssoc_symm_apply`, `prodLexAssoc_apply`
`prodLexCongr` 📖	CompOp	1 math math: `prodLexCongr_apply`
`prodUnique` 📖	CompOp	1 math math: `prodUnique_apply`
`sumLexProdLexDistrib` 📖	CompOp	2 math math: `sumLexProdLexDistrib_symm_apply`, `sumLexProdLexDistrib_apply`
`uniqueProd` 📖	CompOp	1 math math: `uniqueProd_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`prodLexAssoc_apply` 📖	mathematical	—	`DFunLike.coe` `RelIso` `Lex` `instLE` `instLT` `Preorder.toLT` `Preorder.toLE` `RelIso.instFunLike` `prodLexAssoc` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toLex` `ofLex`	—	—
`prodLexAssoc_symm_apply` 📖	mathematical	—	`DFunLike.coe` `RelIso` `Lex` `instLE` `Preorder.toLT` `Preorder.toLE` `instLT` `RelIso.instFunLike` `RelIso.symm` `prodLexAssoc` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toLex` `ofLex`	—	—
`prodLexCongr_apply` 📖	mathematical	—	`DFunLike.coe` `RelIso` `Lex` `instLE` `Preorder.toLT` `Preorder.toLE` `RelIso.instFunLike` `prodLexCongr` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toLex` `OrderIso` `OrderIso.instEquivLike` `ofLex`	—	—
`prodUnique_apply` 📖	mathematical	—	`DFunLike.coe` `OrderIso` `Lex` `instLE` `Preorder.toLT` `PartialOrder.toPreorder` `Preorder.toLE` `instFunLikeOrderIso` `prodUnique` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofLex`	—	—
`sumLexProdLexDistrib_apply` 📖	mathematical	—	`DFunLike.coe` `RelIso` `Lex` `instLE` `Sum.Lex.LT` `Preorder.toLT` `Preorder.toLE` `Sum.Lex.LE` `RelIso.instFunLike` `sumLexProdLexDistrib` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toLex` `Equiv.sumProdDistrib` `ofLex`	—	—
`sumLexProdLexDistrib_symm_apply` 📖	mathematical	—	`DFunLike.coe` `RelIso` `Lex` `Sum.Lex.LE` `instLE` `Preorder.toLT` `Preorder.toLE` `Sum.Lex.LT` `RelIso.instFunLike` `RelIso.symm` `sumLexProdLexDistrib` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toLex` `Equiv.symm` `Equiv.sumProdDistrib` `ofLex`	—	—
`uniqueProd_apply` 📖	mathematical	—	`DFunLike.coe` `OrderIso` `Lex` `instLE` `Preorder.toLT` `instFunLikeOrderIso` `uniqueProd` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofLex`	—	—

RelIso

Definitions

Name	Category	Theorems
`sumLexComplLeft` 📖	CompOp	2 math math: `sumLexComplLeft_symm_apply`, `sumLexComplLeft_apply`
`sumLexComplRight` 📖	CompOp	2 math math: `sumLexComplRight_apply`, `sumLexComplRight_symm_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`sumLexComplLeft_apply` 📖	mathematical	—	`DFunLike.coe` `RelIso` `Subrel` `instFunLike` `sumLexComplLeft` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.sumCompl`	—	—
`sumLexComplLeft_symm_apply` 📖	mathematical	—	`DFunLike.coe` `RelIso` `Subrel` `instFunLike` `sumLexComplLeft` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.sumCompl`	—	—
`sumLexComplRight_apply` 📖	mathematical	—	`DFunLike.coe` `RelIso` `Subrel` `instFunLike` `sumLexComplRight` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.sumCompl`	—	—
`sumLexComplRight_symm_apply` 📖	mathematical	—	`DFunLike.coe` `RelIso` `Subrel` `instFunLike` `sumLexComplRight` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.sumCompl`	—	—

---

← Back to Index