mathlib3
6cf6e8cb - chore(order/filter/basic): golf a few proofs (#14078)

Commit
3 years ago
chore(order/filter/basic): golf a few proofs (#14078) * golf the proof of `mem_generate_iff` by using `sInter_mem`; * use `set.inj_on` in the statement of `filter.eq_of_map_eq_map_inj'`; * golf the proofs of `filter.map_inj` and `filter.comap_ne_bot_iff`.
Author
Parents
Loading