Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-02-08 16:17 1d49f87e

View on Github →

chore(data/finset): golf some proofs (#6101)

  • prove that finset.min' and finset.max' are is_least and is_greatest elements of the corresponding sets;
  • use this fact to golf some proofs; generalize min'_lt_max' to is_glb_lt_is_lub_of_ne;
  • add finset.card_le_one and finset.one_lt_card.

Estimated changes

added theorem finset.card_le_one
added theorem finset.one_lt_card
added theorem finset.is_least_min'
added theorem finset.le_min'_iff
added theorem finset.max'_le_iff
added theorem is_glb_lt_is_lub_of_ne
added theorem le_of_is_lub_le_is_glb