Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-07-07 04:39 095445ee

View on Github →

refactor(order/*): make data.set.basic import order.bounded_lattice (#3285) I have two goals:

  • make it possible to refactor set to use lattice operations;
  • make submonoid.basic independent of data.nat.basic.

Estimated changes

added theorem set.bot_eq_empty
modified theorem set.image_eq_range
added theorem set.inf_eq_inter
added theorem set.le_eq_subset
added theorem set.lt_eq_ssubset
deleted def set.strict_subset
added theorem set.sup_eq_union
deleted theorem set.bot_eq_empty
deleted theorem set.inf_eq_inter
deleted theorem set.le_eq_subset
deleted theorem set.lt_eq_ssubset
deleted theorem set.sup_eq_union
added theorem con.rel_eq_coe
deleted theorem directed.mono
deleted theorem directed.mono_comp
deleted def directed
deleted theorem directed_comp
deleted theorem directed_on.mono
deleted def directed_on
deleted theorem directed_on_iff_directed
deleted theorem directed_on_image
added theorem bot_apply
added theorem inf_apply
added theorem sup_apply
added theorem top_apply
deleted def Inf
modified theorem Inf_apply
deleted def Sup
modified theorem Sup_apply
modified theorem infi_apply
modified theorem supr_apply
added theorem directed.mono
added theorem directed.mono_comp
added def directed
added theorem directed_comp
added theorem directed_of_inf
added theorem directed_of_sup
added theorem directed_on.mono
added def directed_on
added theorem directed_on_image
deleted theorem directed_of_inf
deleted theorem directed_of_mono
deleted theorem directed_of_sup