Lattice

📁 Source: Mathlib/Data/Fintype/Lattice.lean

Statistics

Metric	Count
Definitions	0
Theorems exists_max, exists_min, fold_inf_univ, fold_sup_univ, inf_univ_eq_iInf, mem_inf, sup_univ_eq_iSup	7
Total	7

Finite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_max 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	nonempty_fintype Finset.exists_max_image Finset.univ_nonempty
exists_min 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	nonempty_fintype Finset.exists_min_image Finset.univ_nonempty

Finset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
fold_inf_univ 📖	mathematical	—	fold SemilatticeInf.toMin instCommutativeMin_mathlib instAssociativeMin_mathlib univ Bot.bot OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder	—	instCommutativeMin_mathlib instAssociativeMin_mathlib eq_bot_iff fold_op_rel_iff_and le_inf_iff le_rfl mem_univ
fold_sup_univ 📖	mathematical	—	fold SemilatticeSup.toMax instCommutativeMax_mathlib instAssociativeMax_mathlib univ Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder	—	fold_inf_univ
inf_univ_eq_iInf 📖	mathematical	—	inf Lattice.toSemilatticeInf CompleteLattice.toLattice BoundedOrder.toOrderTop Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder CompleteLattice.toBoundedOrder univ iInf CompleteSemilatticeInf.toInfSet CompleteLattice.toCompleteSemilatticeInf	—	sup_univ_eq_iSup
mem_inf 📖	mathematical	—	Finset instMembership inf Lattice.toSemilatticeInf instLattice CoheytingAlgebra.toOrderTop BiheytingAlgebra.toCoheytingAlgebra BooleanAlgebra.toBiheytingAlgebra booleanAlgebra	—	cons_induction instIsEmptyFalse inf_cons
sup_univ_eq_iSup 📖	mathematical	—	sup Lattice.toSemilatticeSup CompleteLattice.toLattice BoundedOrder.toOrderBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder CompleteLattice.toBoundedOrder univ iSup CompleteSemilatticeSup.toSupSet CompleteLattice.toCompleteSemilatticeSup	—	sup_eq_iSup iSup_pos mem_univ

---

← Back to Index