Commit 2023-01-20 07:09 0a36d065

View on Github →

feat: port Logic.Denumerable (#1682)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Logic/Denumerable.lean

added theorem Denumerable.decode_eq_ofNat

added theorem Denumerable.decode_isSome

added theorem Denumerable.encode_ofNat

added def Denumerable.equiv₂

added def Denumerable.eqv

added def Denumerable.mk'

added def Denumerable.ofEncodableOfInfinite

added def Denumerable.ofEquiv

added theorem Denumerable.ofEquiv_ofNat

added def Denumerable.ofNat

added theorem Denumerable.ofNat_encode

added theorem Denumerable.ofNat_nat

added theorem Denumerable.ofNat_of_decode

added def Denumerable.pair

added theorem Denumerable.prod_nat_ofNat

added theorem Denumerable.prod_ofNat_val

added theorem Denumerable.sigma_ofNat_val

added theorem Nat.Subtype.coe_comp_ofNat_range

added def Nat.Subtype.denumerable

added theorem Nat.Subtype.exists_succ

added theorem Nat.Subtype.le_succ_of_forall_lt_le

added theorem Nat.Subtype.lt_succ_iff_le

added theorem Nat.Subtype.lt_succ_self

added def Nat.Subtype.ofNat

added theorem Nat.Subtype.ofNat_range

added theorem Nat.Subtype.ofNat_surjective

added theorem Nat.Subtype.ofNat_surjective_aux

added def Nat.Subtype.succ

added theorem Nat.Subtype.succ_le_of_lt

added theorem nonempty_denumerable

Modified Mathlib/Logic/Encodable/Basic.lean