Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-06-14 16:36 0d052998

View on Github →

chore(data/finset): rename ext/ext'/ext_iff (#3069) Now

  • ext is the @[ext] lemma;
  • ext_iff is the lemma s₁ = s₂ ↔ ∀ a, a ∈ s₁ ↔ a ∈ s₂. Also add 2 norm_cast attributes and a lemma ssubset_iff_of_subset.

Estimated changes

modified theorem finset.coe_inj
deleted theorem finset.ext'
modified theorem finset.ext
added theorem finset.ext_iff
modified theorem finset.mem_coe