Commit 2022-12-26 12:39 ba5b7d90

View on Github →

feat: port data.nat.pairing (#1172) Port of data.nat.pairing

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Nat/Pairing.lean

added theorem Nat.add_le_mkpair

added theorem Nat.left_le_mkpair

added theorem Nat.max_sq_add_min_le_mkpair

added def Nat.mkpair

added def Nat.mkpairEquiv

added theorem Nat.mkpair_eq_mkpair

added theorem Nat.mkpair_lt_max_add_one_sq

added theorem Nat.mkpair_lt_mkpair_left

added theorem Nat.mkpair_lt_mkpair_right

added theorem Nat.mkpair_unpair'

added theorem Nat.mkpair_unpair

added theorem Nat.right_le_mkpair

added theorem Nat.surjective_unpair

added def Nat.unpair

added theorem Nat.unpair_add_le

added theorem Nat.unpair_left_le

added theorem Nat.unpair_lt

added theorem Nat.unpair_mkpair

added theorem Nat.unpair_right_le

added theorem Nat.unpair_zero

added theorem Set.interᵢ_unpair

added theorem Set.unionᵢ_unpair

added theorem Set.unionᵢ_unpair_prod

added theorem infᵢ_unpair

added theorem supᵢ_unpair