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 theorem real.exists_floor
modified theorem real.mk_add
modified theorem real.mk_mul
modified theorem real.mk_neg
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
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_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_singleton
added theorem lattice.cSup_union
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 theorem lattice.inf_le_left
modified theorem lattice.inf_le_right
modified theorem lattice.le_sup_left
modified theorem lattice.le_sup_right