mathlib
a1a1fbd7 - feat(set_theory/zfc/basic): `⊆` is reflexive, transitive, antisymmetric (#15551)

Commit
3 years ago
feat(set_theory/zfc/basic): `⊆` is reflexive, transitive, antisymmetric (#15551) This gives us access to the `subset_refl`, `subset_trans`, `subset_antisymm` lemmas defined elsewhere.
Author
Parents
Loading