Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-19 14:04 ba6a9858

View on Github →

feat(order/cover): define wcovby (#13424)

  • This defines the reflexive closure of covby, which I call wcovby ("weakly covered by")
  • This is useful, since some results about covby still hold for wcovby.
  • Use wcovby in the proofs of the properties for covby.
  • Also define wcovby_insert (the motivating example, since I really want (wcovby_insert _ _).eq_or_eq)

Estimated changes

modified theorem apply_covby_apply_iff
added theorem apply_wcovby_apply_iff
modified theorem covby.image
modified theorem covby.of_image
added theorem not_wcovby_iff
added theorem set.covby_insert
added theorem set.wcovby_insert
added theorem wcovby.Icc_eq
added theorem wcovby.Ico_subset
added theorem wcovby.Ioc_subset
added theorem wcovby.Ioo_eq
added theorem wcovby.covby_of_lt
added theorem wcovby.covby_of_ne
added theorem wcovby.covby_of_not_le
added theorem wcovby.eq_or_eq
added theorem wcovby.image
added theorem wcovby.le
added theorem wcovby.le_and_le_iff
added theorem wcovby.of_image
added theorem wcovby.refl
added theorem wcovby.rfl
added theorem wcovby.wcovby_iff_le
added def wcovby
added theorem wcovby_iff_covby_or_eq
added theorem wcovby_of_eq_or_eq
added theorem wcovby_of_le_of_le
added theorem order.pred_wcovby
added theorem order.wcovby_succ