mathlib
0d052998
- chore(data/finset): rename `ext`/`ext'`/`ext_iff` (#3069)
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
5 years ago
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`.
Author
urkud
Parents
1f16da1b
Loading