Commit 2022-07-21 13:52 8672734e

View on Github →

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.

Estimated changes

Modified src/set_theory/zfc/ordinal.lean

added theorem Set.empty_is_transitive

added theorem Set.is_transitive.sUnion'

deleted theorem Set.is_transitive.sUnion

modified theorem Set.is_transitive.subset_of_mem

modified theorem Set.is_transitive_iff_mem_trans

modified theorem Set.is_transitive_iff_sUnion_subset

modified theorem Set.is_transitive_iff_subset_powerset