Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-09-29 09:37 0de54327

View on Github →

feat(data/W/cardinal): results about cardinality of W-types (#9210)

Estimated changes

Modified archive/examples/prop_encodable.lean

Renamed src/data/W.lean to src/data/W/basic.lean

added def W_type.elim

added theorem W_type.elim_injective

added def W_type.equiv_sigma

added theorem W_type.infinite_of_nonempty_of_is_empty

added def W_type.of_sigma

added theorem W_type.of_sigma_to_sigma

added def W_type.to_sigma

added theorem W_type.to_sigma_of_sigma

Created src/data/W/cardinal.lean

added theorem W_type.cardinal_mk_eq_sum

added theorem W_type.cardinal_mk_le_max_omega_of_fintype

added theorem W_type.cardinal_mk_le_of_le

Modified src/data/pfunctor/univariate/basic.lean