mathlib
f0b3759a - chore(set_theory/zfc/basic): reverse `sInter_coe` (#18773)

Commit
2 years ago
chore(set_theory/zfc/basic): reverse `sInter_coe` (#18773) It now matches `coe_sUnion`, and works as a `norm_cast` lemma. Mathlib 4: https://github.com/leanprover-community/mathlib4/pull/3345
Author
Parents
Loading