Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-02-08 22:50 5dd34192

View on Github →

feat(order/conditionally_complete_lattice): Conditionally complete lattices

Estimated changes

Modified data/real/basic.lean

modified theorem real.exists_floor

modified theorem real.mk_add

modified theorem real.mk_mul

modified theorem real.mk_neg

Modified data/set/basic.lean

modified theorem set.inter_univ

modified theorem set.subset_union_left

modified theorem set.subset_union_right

added theorem set.union_empty_iff

modified theorem set.union_subset_iff

modified theorem set.univ_inter

Created order/conditionally_complete_lattice.lean

added theorem bdd_above.mk

added def bdd_above

added theorem bdd_above_Int1

added theorem bdd_above_Int2

added theorem bdd_above_bot

added theorem bdd_above_empty

added theorem bdd_above_finite

added theorem bdd_above_finite_union

added theorem bdd_above_insert

added theorem bdd_above_singleton

added theorem bdd_above_subset

added theorem bdd_above_top

added theorem bdd_above_union

added theorem bdd_below.mk

added def bdd_below

added theorem bdd_below_Int1

added theorem bdd_below_Int2

added theorem bdd_below_empty

added theorem bdd_below_finite

added theorem bdd_below_finite_union

added theorem bdd_below_insert

added theorem bdd_below_singleton

added theorem bdd_below_subset

added theorem bdd_below_union

added theorem lattice.cInf_insert

added theorem lattice.cInf_intro

added theorem lattice.cInf_le

added theorem lattice.cInf_le_cInf

added theorem lattice.cInf_le_cSup

added theorem lattice.cInf_le_of_le

added theorem lattice.cInf_lt_of_lt

added theorem lattice.cInf_of_in_of_le

added theorem lattice.cInf_singleton

added theorem lattice.cInf_union

added theorem lattice.cSup_insert

added theorem lattice.cSup_inter_le

added theorem lattice.cSup_intro

added theorem lattice.cSup_le

added theorem lattice.cSup_le_cSup

added theorem lattice.cSup_le_iff

added theorem lattice.cSup_of_in_of_le

added theorem lattice.cSup_singleton

added theorem lattice.cSup_union

added theorem lattice.exists_lt_of_cInf_lt

added theorem lattice.exists_lt_of_lt_cSup

added theorem lattice.le_cInf

added theorem lattice.le_cInf_iff

added theorem lattice.le_cInf_inter

added theorem lattice.le_cSup

added theorem lattice.le_cSup_of_le

added theorem lattice.lt_cSup_of_lt

Modified order/lattice.lean

modified theorem lattice.inf_le_left

modified theorem lattice.inf_le_right

modified theorem lattice.le_sup_left

modified theorem lattice.le_sup_right