Commit 2026-10-01 17:54 8b426c3a

View on Github →

feat(Data/Sym/Sym2/Card): cardinality theorems about Sym2 α (#36442)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/Set/Image.lean

added theorem Set.preimage_singleton

Modified Mathlib/Data/Sym/Sym2.lean

added theorem Sym2.mk_fiber

added theorem Sym2.mk_fiber_of_isDiag

added theorem Sym2.mk_fst_out_snd_out

Created Mathlib/Data/Sym/Sym2/Card.lean

added theorem Sym2.cardinalMk_diagSet

added theorem Sym2.cardinalMk_prod_eq_two_mul_cardinalMk_fromRel

added theorem Sym2.cardinalMk_prod_le

added theorem Sym2.cardinalMk_prod_le_two_mul_cardinalMk_fromRel

added theorem Sym2.encard_diagSet

added theorem Sym2.encard_mk_fiber_le

added theorem Sym2.finite_fromRel_iff

added theorem Sym2.finite_mk_fiber

added theorem Sym2.finite_sym2_iff

added theorem Sym2.infinite_fromRel_iff

added theorem Sym2.infinite_sym2_iff

added theorem Sym2.ncard_mk_fiber

added theorem Sym2.ncard_mk_fiber_eq_card_toFinset

added theorem Sym2.ncard_mk_fiber_of_isDiag

added theorem Sym2.ncard_mk_fiber_of_not_isDiag

added theorem Sym2.two_mul_cardinalMk_diagSet_compl_add_cardinalMk

added theorem Sym2.two_mul_cardinalMk_sym2

added theorem Sym2.two_mul_encard_diagSet_compl_add_enatCard