Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-01-23 16:35 0e6c3589

View on Github →

feat(set_theory/cardinal): more lemmas on cardinality (#595)

Estimated changes

Modified src/data/set/basic.lean

added def set.image_factorization

added theorem set.image_factorization_eq

added def set.range_factorization

added theorem set.range_factorization_eq

added theorem set.surjective_onto_image

added theorem set.surjective_onto_range

Modified src/set_theory/cardinal.lean

added theorem cardinal.mk_image_le

added theorem cardinal.mk_le_of_injective

added theorem cardinal.mk_le_of_surjective

added theorem cardinal.mk_quot_le

added theorem cardinal.mk_quotient_le

added theorem cardinal.mk_range_le

added theorem cardinal.mk_subtype_le

added theorem cardinal.mk_univ