Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-05-25 05:55 1991869f

View on Github →

feat(order/bounded_lattice): with_bot, with_top structures

Estimated changes

Modified data/finset.lean

added def finset.inf

added theorem finset.inf_empty

added theorem finset.inf_insert

added theorem finset.inf_le

added theorem finset.inf_mono

added theorem finset.inf_mono_fun

added theorem finset.inf_singleton

added theorem finset.inf_union

added theorem finset.le_inf

added theorem finset.le_sup

added theorem finset.max_eq_inf_with_top

added theorem finset.max_eq_sup_with_bot

added theorem finset.singleton_bind

modified theorem finset.subset_iff

added def finset.sup

added theorem finset.sup_empty

added theorem finset.sup_insert

added theorem finset.sup_le

added theorem finset.sup_mono

added theorem finset.sup_mono_fun

added theorem finset.sup_singleton

added theorem finset.sup_union

Modified data/finsupp.lean

added theorem finsupp.erase_add_single

added theorem finsupp.induction₂

modified theorem finsupp.single_add_erase

Modified data/option.lean

added theorem option.ext

Modified linear_algebra/multivariate_polynomial.lean

deleted theorem finset.bind_singleton2

deleted theorem finset.le_sup

deleted def finset.sup

deleted theorem finset.sup_empty

deleted theorem finset.sup_insert

deleted theorem finset.sup_le

deleted theorem finset.sup_mono

deleted theorem finset.sup_mono_fun

deleted theorem finset.sup_singleton

deleted theorem finset.sup_union

Modified order/bounded_lattice.lean

added theorem lattice.with_bot.some_le

added theorem lattice.with_bot.some_le_some

added def lattice.with_bot

added theorem lattice.with_top.le_some

added theorem lattice.with_top.some_le_some

added def lattice.with_top

Modified order/lattice.lean