Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-07 15:09 8a60fd75

View on Github →

refactor(data/ennreal/basic): prove has_ordered_sub instance (#9582)

  • Give has_sub and has_ordered_sub instances on with_top α.
  • This gives a new subtraction on ennreal. The lemma ennreal.sub_eq_Inf proves that it is equal to the old value.
  • Simplify many proofs about sub on ennreal
  • Proofs that are instantiations of more general lemmas will be removed in a subsequent PR
  • Many lemmas that require add_le_cancellable in general are reformulated using ≠ ∞
  • Lemmas are reordered, but no lemmas are renamed, removed, or have a different type. Some @[simp] tags are removed if a more general simp lemma applies.
  • Minor: generalize preorder to has_le in has_ordered_sub (not necessary for this PR, but useful in another (abandoned) branch).

Estimated changes

added theorem with_top.coe_sub
added theorem with_top.sub_top
added theorem with_top.top_sub_coe
modified theorem ennreal.add_sub_self'
modified theorem ennreal.add_sub_self
added theorem ennreal.cancel_coe
added theorem ennreal.cancel_of_lt'
added theorem ennreal.cancel_of_lt
added theorem ennreal.cancel_of_ne
modified theorem ennreal.coe_sub
added theorem ennreal.sub_eq_Inf
modified theorem ennreal.sub_eq_of_add_eq
added theorem ennreal.sub_eq_top_iff
added theorem ennreal.sub_ne_top
modified theorem ennreal.sub_self
modified theorem ennreal.sub_top
modified theorem ennreal.sub_zero
modified theorem ennreal.top_sub_coe
modified theorem ennreal.zero_sub