mathlib3
8672734e - feat(set_theory/zfc/ordinal): more lemmas on transitive sets (#15548)

Commit
3 years ago
feat(set_theory/zfc/ordinal): more lemmas on transitive sets (#15548) We add `empty_is_transitive`, `is_transitive.inter`, and `is_transitive.sUnion'`. We also add a `variables` block.
Author
Parents
Loading