Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-02-25 14:16 450dcdf9

View on Github →

refactor(order/bounds): use dot notation, reorder, prove more properties (#2028)

  • refactor(order/bounds): use dot notation, prove more properties Also make parts of complete_lattice and conditionally_complete_lattice use these lemmas.
  • Comments
  • Add a module docstring
  • Fixes from review, +4 lemmas about images
  • Fix a typo in the previous commit
  • Update src/order/bounds.lean
  • Update src/order/bounds.lean

Estimated changes

added theorem bdd_above.insert
deleted theorem bdd_above.mk
added theorem bdd_above.mono
added theorem bdd_above.union
modified def bdd_above
added theorem bdd_above_Icc
added theorem bdd_above_Ico
added theorem bdd_above_Iic
added theorem bdd_above_Iio
added theorem bdd_above_Ioc
added theorem bdd_above_Ioo
modified theorem bdd_above_empty
modified theorem bdd_above_iff_subset_Iic
modified theorem bdd_above_insert
deleted theorem bdd_above_inter_left
deleted theorem bdd_above_inter_right
modified theorem bdd_above_singleton
deleted theorem bdd_above_subset
deleted theorem bdd_above_top
modified theorem bdd_above_union
added theorem bdd_below.insert
deleted theorem bdd_below.mk
added theorem bdd_below.mono
added theorem bdd_below.union
modified def bdd_below
added theorem bdd_below_Ici
added theorem bdd_below_Ioi
deleted theorem bdd_below_bot
modified theorem bdd_below_empty
modified theorem bdd_below_iff_subset_Ici
modified theorem bdd_below_insert
deleted theorem bdd_below_inter_left
deleted theorem bdd_below_inter_right
modified theorem bdd_below_singleton
deleted theorem bdd_below_subset
modified theorem bdd_below_union
deleted theorem eq_of_is_glb_of_is_glb
deleted theorem eq_of_is_lub_of_is_lub
added theorem is_glb.bdd_below
added theorem is_glb.insert
added theorem is_glb.lower_bounds_eq
added theorem is_glb.nonempty
added theorem is_glb.union
added theorem is_glb.unique
modified theorem is_glb_Icc
modified theorem is_glb_Ici
modified theorem is_glb_Ico
modified theorem is_glb_Ioc
modified theorem is_glb_Ioi
modified theorem is_glb_Ioo
modified theorem is_glb_empty
deleted theorem is_glb_iff_eq_of_is_glb
deleted theorem is_glb_iff_inf_eq
deleted theorem is_glb_insert_inf
added theorem is_glb_le_is_lub
modified theorem is_glb_lt_iff
added theorem is_glb_pair
modified theorem is_glb_singleton
deleted theorem is_glb_union_inf
added theorem is_glb_univ
added theorem is_greatest.bdd_above
added theorem is_greatest.insert
added theorem is_greatest.is_lub
added theorem is_greatest.nonempty
added theorem is_greatest.union
added theorem is_greatest.unique
added theorem is_greatest_Icc
added theorem is_greatest_Iic
added theorem is_greatest_Ioc
added theorem is_greatest_pair
added theorem is_greatest_singleton
added theorem is_greatest_union_iff
added theorem is_greatest_univ
added theorem is_least.bdd_below
added theorem is_least.insert
added theorem is_least.is_glb
added theorem is_least.nonempty
added theorem is_least.union
added theorem is_least.unique
added theorem is_least_Icc
added theorem is_least_Ici
added theorem is_least_Ico
added theorem is_least_pair
added theorem is_least_singleton
added theorem is_least_union_iff
added theorem is_least_univ
added theorem is_lub.bdd_above
added theorem is_lub.insert
added theorem is_lub.nonempty
added theorem is_lub.union
added theorem is_lub.unique
added theorem is_lub.upper_bounds_eq
modified theorem is_lub_Icc
modified theorem is_lub_Ico
modified theorem is_lub_Iic
modified theorem is_lub_Iio
modified theorem is_lub_Ioc
modified theorem is_lub_Ioo
modified theorem is_lub_empty
deleted theorem is_lub_iff_eq_of_is_lub
deleted theorem is_lub_iff_sup_eq
deleted theorem is_lub_insert_sup
modified theorem is_lub_le_iff
added theorem is_lub_lt_iff
added theorem is_lub_pair
modified theorem is_lub_singleton
deleted theorem is_lub_union_sup
added theorem is_lub_univ
modified theorem le_is_glb_iff
added theorem lower_bound_Ioc
added theorem lower_bounds_Icc
added theorem lower_bounds_Ici
added theorem lower_bounds_Ico
added theorem lower_bounds_Ioi
added theorem lower_bounds_Ioo
added theorem lower_bounds_empty
added theorem lower_bounds_insert
modified theorem lower_bounds_mono
added theorem lower_bounds_mono_mem
added theorem lower_bounds_mono_set
added theorem lower_bounds_singleton
added theorem lower_bounds_union
added theorem lt_is_glb_iff
modified theorem lt_is_lub_iff
deleted theorem mem_lower_bounds_image
deleted theorem mem_upper_bounds_image
added theorem monotone.map_bdd_above
added theorem monotone.map_bdd_below
added theorem monotone.map_is_least
deleted theorem nonempty_of_is_glb
deleted theorem nonempty_of_is_lub
added theorem upper_bounds_Icc
added theorem upper_bounds_Ico
added theorem upper_bounds_Iic
added theorem upper_bounds_Iio
added theorem upper_bounds_Ioc
added theorem upper_bounds_Ioo
added theorem upper_bounds_empty
added theorem upper_bounds_insert
modified theorem upper_bounds_mono
added theorem upper_bounds_mono_mem
added theorem upper_bounds_mono_set
added theorem upper_bounds_singleton
added theorem upper_bounds_union
modified theorem lattice.Inf_le_Sup
added theorem lattice.Inf_pair
added theorem lattice.Sup_pair
modified theorem lattice.infi_const
modified theorem lattice.is_glb_Inf
deleted theorem lattice.is_glb_iff_Inf_eq
modified theorem lattice.is_glb_infi
modified theorem lattice.is_lub_Sup
deleted theorem lattice.is_lub_iff_Sup_eq
modified theorem lattice.is_lub_supr
modified theorem lattice.supr_const
added theorem lattice.cInf_Ici
modified theorem lattice.cInf_insert
deleted theorem lattice.cInf_interval
modified theorem lattice.cInf_le_cSup
deleted theorem lattice.cInf_of_mem_of_le
modified theorem lattice.cInf_union
added theorem lattice.cSup_Iic
modified theorem lattice.cSup_insert
deleted theorem lattice.cSup_interval
modified theorem lattice.cSup_le_iff
deleted theorem lattice.cSup_of_mem_of_le
modified theorem lattice.cSup_union
modified theorem lattice.is_glb_cInf
modified theorem lattice.is_lub_cSup
modified theorem lattice.le_cInf_iff