Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-12-07 13:49 04559629

View on Github →

refactor(order/bounds,*): move code around to make order.bounds not depend on complete_lattice (#1783)

  • refactor(order/bounds,*): move code around to make order.bounds not depend on complete_lattice In another PR I'm going to prove more facts in order/bounds, then replace many proofs of lemmas about (c)Sup/(c)Inf with references to lemmas about is_lub/is_glb.
  • Move more code to basic, rewrite the only remaining proof in default
  • Rename
  • Add default.lean

Estimated changes

deleted theorem set.eq_of_Ico_disjoint
deleted theorem set.is_glb_Icc
deleted theorem set.is_glb_Ici
deleted theorem set.is_glb_Ico
deleted theorem set.is_glb_Ioc
deleted theorem set.is_glb_Ioi
deleted theorem set.is_glb_Ioo
deleted theorem set.is_lub_Icc
deleted theorem set.is_lub_Ico
deleted theorem set.is_lub_Iic
deleted theorem set.is_lub_Iio
deleted theorem set.is_lub_Ioc
deleted theorem set.is_lub_Ioo
added theorem bdd_above.mk
added def bdd_above
added theorem bdd_above_empty
added theorem bdd_above_insert
added theorem bdd_above_inter_left
added theorem bdd_above_inter_right
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_bot
added theorem bdd_below_empty
added theorem bdd_below_insert
added theorem bdd_below_inter_left
added theorem bdd_below_inter_right
added theorem bdd_below_singleton
added theorem bdd_below_subset
added theorem bdd_below_union
added theorem is_glb_Icc
added theorem is_glb_Ici
added theorem is_glb_Ico
deleted theorem is_glb_Inf
added theorem is_glb_Ioc
added theorem is_glb_Ioi
added theorem is_glb_Ioo
deleted theorem is_glb_iff_Inf_eq
deleted theorem is_glb_iff_infi_eq
deleted theorem is_glb_infi
added theorem is_lub_Icc
added theorem is_lub_Ico
added theorem is_lub_Iic
added theorem is_lub_Iio
added theorem is_lub_Ioc
added theorem is_lub_Ioo
deleted theorem is_lub_Sup
deleted theorem is_lub_iff_Sup_eq
deleted theorem is_lub_iff_supr_eq
deleted theorem is_lub_supr
deleted theorem bdd_above.mk
deleted def bdd_above
deleted theorem bdd_above_empty
deleted theorem bdd_above_finite
deleted theorem bdd_above_finite_union
deleted theorem bdd_above_insert
deleted theorem bdd_above_inter_left
deleted theorem bdd_above_inter_right
deleted theorem bdd_above_singleton
deleted theorem bdd_above_subset
deleted theorem bdd_above_top
deleted theorem bdd_above_union
deleted theorem bdd_below.mk
deleted def bdd_below
deleted theorem bdd_below_bot
deleted theorem bdd_below_empty
deleted theorem bdd_below_finite
deleted theorem bdd_below_finite_union
deleted theorem bdd_below_insert
deleted theorem bdd_below_inter_left
deleted theorem bdd_below_inter_right
deleted theorem bdd_below_singleton
deleted theorem bdd_below_subset
deleted theorem bdd_below_union