Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-05-25 01:14 94dc0677

View on Github →

refactor(order/lattice): move top/bot to bounded_lattice

Estimated changes

added theorem lattice.bot_inf_eq
added theorem lattice.bot_le
added theorem lattice.bot_sup_eq
added theorem lattice.bot_unique
added theorem lattice.eq_bot_iff
added theorem lattice.eq_top_iff
added theorem lattice.inf_bot_eq
added theorem lattice.inf_eq_top_iff
added theorem lattice.inf_top_eq
added theorem lattice.le_bot_iff
added theorem lattice.le_top
added theorem lattice.not_lt_bot
added theorem lattice.not_top_lt
added theorem lattice.sup_bot_eq
added theorem lattice.sup_eq_bot_iff
added theorem lattice.sup_top_eq
added theorem lattice.top_inf_eq
added theorem lattice.top_le_iff
added theorem lattice.top_sup_eq
added theorem lattice.top_unique
deleted theorem lattice.bot_inf_eq
deleted theorem lattice.bot_le
deleted theorem lattice.bot_sup_eq
deleted theorem lattice.bot_unique
deleted theorem lattice.eq_bot_iff
deleted theorem lattice.eq_top_iff
deleted theorem lattice.inf_bot_eq
deleted theorem lattice.inf_eq_top_iff
deleted theorem lattice.inf_top_eq
deleted theorem lattice.le_bot_iff
deleted theorem lattice.le_top
deleted theorem lattice.not_lt_bot
deleted theorem lattice.not_top_lt
deleted theorem lattice.sup_bot_eq
deleted theorem lattice.sup_eq_bot_iff
deleted theorem lattice.sup_top_eq
deleted theorem lattice.top_inf_eq
deleted theorem lattice.top_le_iff
deleted theorem lattice.top_sup_eq
deleted theorem lattice.top_unique