Commit 2023-04-25 23:03 f0b3759a
View on Github →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
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