Lattice

📁 Source: Mathlib/Order/BoundedOrder/Lattice.lean

Statistics

Metric	Count
Definitions	0
Theorems induction_top, induction_bot, bot_inf_eq, bot_sup_eq, inf_bot_eq, inf_eq_top_iff, inf_top_eq, max_bot_left, max_bot_right, max_eq_bot, max_eq_top, max_ne_top, max_top_left, max_top_right, min_bot_left, min_bot_right, min_eq_bot, min_eq_top, min_ne_bot, min_top_left, min_top_right, sup_bot_eq, sup_eq_bot_iff, sup_top_eq, top_inf_eq, top_sup_eq	26
Total	26

WellFoundedGT

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
induction_top 📖	mathematical	Preorder.toLT	Top.top OrderTop.toTop Preorder.toLE	—	Mathlib.Tactic.Contrapose.contrapose₁ induction

WellFoundedLT

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
induction_bot 📖	mathematical	Preorder.toLT	Bot.bot OrderBot.toBot Preorder.toLE	—	Mathlib.Tactic.Contrapose.contrapose₁ Mathlib.Tactic.Push.not_exists induction

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bot_inf_eq 📖	mathematical	—	SemilatticeInf.toMin Bot.bot OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder	—	inf_of_le_left bot_le
bot_sup_eq 📖	mathematical	—	SemilatticeSup.toMax Bot.bot OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder	—	sup_of_le_right bot_le
inf_bot_eq 📖	mathematical	—	SemilatticeInf.toMin Bot.bot OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder	—	inf_of_le_right bot_le
inf_eq_top_iff 📖	mathematical	—	SemilatticeInf.toMin Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder	—	eq_top_iff le_inf_iff top_le_iff
inf_top_eq 📖	mathematical	—	SemilatticeInf.toMin Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder	—	inf_of_le_left le_top
max_bot_left 📖	mathematical	—	SemilatticeSup.toMax Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder Bot.bot OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf	—	bot_sup_eq
max_bot_right 📖	mathematical	—	SemilatticeSup.toMax Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder Bot.bot OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf	—	sup_bot_eq
max_eq_bot 📖	mathematical	—	SemilatticeSup.toMax Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder Bot.bot OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf	—	sup_eq_bot_iff
max_eq_top 📖	mathematical	—	SemilatticeSup.toMax Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder	—	top_le_iff le_sup_iff
max_ne_top 📖	—	—	—	—	—
max_top_left 📖	mathematical	—	SemilatticeSup.toMax Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder	—	top_sup_eq
max_top_right 📖	mathematical	—	SemilatticeSup.toMax Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder	—	sup_top_eq
min_bot_left 📖	mathematical	—	SemilatticeInf.toMin Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Bot.bot OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder	—	bot_inf_eq
min_bot_right 📖	mathematical	—	SemilatticeInf.toMin Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Bot.bot OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder	—	inf_bot_eq
min_eq_bot 📖	mathematical	—	SemilatticeInf.toMin Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Bot.bot OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder	—	—
min_eq_top 📖	mathematical	—	SemilatticeInf.toMin Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup	—	inf_eq_top_iff
min_ne_bot 📖	—	—	—	—	—
min_top_left 📖	mathematical	—	SemilatticeInf.toMin Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup	—	top_inf_eq
min_top_right 📖	mathematical	—	SemilatticeInf.toMin Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup	—	inf_top_eq
sup_bot_eq 📖	mathematical	—	SemilatticeSup.toMax Bot.bot OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder	—	sup_of_le_left bot_le
sup_eq_bot_iff 📖	mathematical	—	SemilatticeSup.toMax Bot.bot OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder	—	eq_bot_iff sup_le_iff
sup_top_eq 📖	mathematical	—	SemilatticeSup.toMax Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder	—	sup_of_le_right le_top
top_inf_eq 📖	mathematical	—	SemilatticeInf.toMin Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder	—	inf_of_le_right le_top
top_sup_eq 📖	mathematical	—	SemilatticeSup.toMax Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder	—	sup_of_le_left le_top

---

← Back to Index