Commit 2023-03-26 23:49 c5dd9310

View on Github →

feat(set_theory/zfc/basic): tweak Class hom lemmas (#18295) This PR renames a bunch of hom lemmas to better match the style of the rest of mathlib, and tags them as norm_cast. We also add the corresponding lemmas for the union.

Estimated changes

Modified src/set_theory/zfc/basic.lean

added theorem Class.coe_apply

added theorem Class.coe_diff

added theorem Class.coe_empty

added theorem Class.coe_insert

added theorem Class.coe_inter

added theorem Class.coe_mem

deleted theorem Class.coe_mem_powerset

added theorem Class.coe_powerset

added theorem Class.coe_sUnion

added theorem Class.coe_sep

added theorem Class.coe_subset

added theorem Class.coe_union

deleted theorem Class.diff_hom

deleted theorem Class.empty_hom

deleted theorem Class.insert_hom

deleted theorem Class.inter_hom

deleted theorem Class.mem_hom_left

deleted theorem Class.mem_hom_right

added theorem Class.powerset_apply

deleted theorem Class.powerset_hom

added theorem Class.sUnion_apply

deleted theorem Class.sUnion_hom

deleted theorem Class.sep_hom

deleted theorem Class.subset_hom

deleted theorem Class.union_hom