Commit 2024-10-12 08:01 0405d97a

View on Github →

feat(SetTheory/Cardinal/Basic): congruency theorems for cardinalities of sigmas (#16824) Add various congruency lemmas for Cardinal.mk.

Estimated changes

Modified Mathlib/SetTheory/Cardinal/Basic.lean

added theorem Cardinal.mk_pi_congr'

added theorem Cardinal.mk_pi_congr

added theorem Cardinal.mk_pi_congrRight

added theorem Cardinal.mk_pi_congrRight_prop

added theorem Cardinal.mk_pi_congr_lift

added theorem Cardinal.mk_pi_congr_prop

added theorem Cardinal.mk_psigma_congrRight

added theorem Cardinal.mk_psigma_congrRight_prop

added theorem Cardinal.mk_sigma_congr'

added theorem Cardinal.mk_sigma_congr

added theorem Cardinal.mk_sigma_congrRight

added theorem Cardinal.mk_sigma_congr_lift