Pairing

📁 Source: Mathlib/Data/Nat/Pairing.lean

Statistics

Metric	Count
Definitions pair, pairEquiv, unpair	3
Theorems add_le_pair, left_le_pair, max_sq_add_min_le_pair, pairEquiv_apply, pairEquiv_symm_apply, pair_eq_of_unpair_eq, pair_eq_pair, pair_lt_max_add_one_sq, pair_lt_pair_left, pair_lt_pair_right, pair_unpair, right_le_pair, surjective_unpair, unpair_add_le, unpair_left_le, unpair_lt, unpair_pair, unpair_right_le, unpair_zero, iInter_unpair, iUnion_unpair, iUnion_unpair_prod, iInf_unpair, iSup_unpair	24
Total	27

Nat

Definitions

Name	Category	Theorems
pair 📖	CompOp	27 math math: Partrec.prec', pairEquiv_apply, pair_lt_pair_right, Primrec'.natPair, Encodable.encode_sigma_val, pair_lt_pair_left, Partrec.rfind', Partrec.Code.eval_prec_succ, pair_eq_pair, Primrec.prec1, left_le_pair, right_le_pair, max_sq_add_min_le_pair, ack_pair_lt, pair_lt_max_add_one_sq, Primrec₂.natPair, pair_unpair, Encodable.encode_prod_val, Partrec.Code.smn, add_le_pair, unpair_pair, Encodable.encode_list_cons, Primrec.swap, Primrec.casesOn', Partrec.Code.eval_prec_zero, pair_eq_of_unpair_eq, Partrec.Code.eval_curry
pairEquiv 📖	CompOp	2 math math: pairEquiv_apply, pairEquiv_symm_apply
unpair 📖	CompOp	25 math math: Denumerable.prod_ofNat_val, Encodable.decode_sigma_val, iInf_unpair, Primrec'.unpair₁, Set.iInter_unpair, iSup_unpair, Set.iUnion_unpair_prod, unpair_lt, unpair_zero, Denumerable.list_ofNat_succ, Primrec'.unpair₂, Primrec.unpair, pairEquiv_symm_apply, Computable.unpair, Denumerable.sigma_ofNat_val, surjective_unpair, Encodable.decode_prod_val, pair_unpair, unpair_right_le, unpair_add_le, unpair_pair, Encodable.decode_list_succ, Denumerable.prod_nat_ofNat, Set.iUnion_unpair, unpair_left_le

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_le_pair 📖	mathematical	—	pair	—	—
left_le_pair 📖	mathematical	—	pair	—	unpair_pair unpair_left_le
max_sq_add_min_le_pair 📖	mathematical	—	pair	—	pair.eq_1 lt_or_ge max_eq_right LT.lt.le min_eq_left le_refl LE.le.not_gt max_eq_left min_eq_right
pairEquiv_apply 📖	mathematical	—	DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike pairEquiv pair	—	—
pairEquiv_symm_apply 📖	mathematical	—	DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Equiv.symm pairEquiv unpair	—	—
pair_eq_of_unpair_eq 📖	mathematical	unpair	pair	—	pair_unpair
pair_eq_pair 📖	mathematical	—	pair	—	Equiv.injective
pair_lt_max_add_one_sq 📖	mathematical	—	pair	—	sup_of_le_right sup_of_le_left not_lt
pair_lt_pair_left 📖	mathematical	—	pair	—	not_lt not_lt_of_gt lt_of_le_of_lt
pair_lt_pair_right 📖	mathematical	—	pair	—	lt_trans sqrt_lt sqrt_add_eq le_trans not_lt
pair_unpair 📖	mathematical	—	pair unpair	—	sqrt_le sqrt_le_add LE.le.not_gt le_of_not_gt
right_le_pair 📖	mathematical	—	pair	—	le_trans
surjective_unpair 📖	mathematical	—	unpair	—	Equiv.surjective
unpair_add_le 📖	mathematical	—	unpair	—	LE.le.trans_eq add_le_pair pair_unpair
unpair_left_le 📖	mathematical	—	unpair	—	unpair_zero le_of_lt unpair_lt
unpair_lt 📖	mathematical	—	unpair	—	lt_of_lt_of_le sqrt_le_self sqrt_pos lt_of_le_of_lt
unpair_pair 📖	mathematical	—	unpair pair	—	sqrt_add_eq le_trans le_of_lt le_of_not_gt
unpair_right_le 📖	mathematical	—	unpair	—	pair_unpair right_le_pair
unpair_zero 📖	mathematical	—	unpair Prod.instZero	—	unpair.eq_1

Set

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
iInter_unpair 📖	mathematical	—	iInter Nat.unpair	—	iInf_unpair
iUnion_unpair 📖	mathematical	—	iUnion Nat.unpair	—	iSup_unpair
iUnion_unpair_prod 📖	mathematical	—	iUnion SProd.sprod Set instSProd Nat.unpair	—	iUnion_prod Function.Surjective.iUnion_comp Nat.surjective_unpair

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
iInf_unpair 📖	mathematical	—	iInf CompleteSemilatticeInf.toInfSet CompleteLattice.toCompleteSemilatticeInf Nat.unpair	—	iSup_unpair
iSup_unpair 📖	mathematical	—	iSup CompleteSemilatticeSup.toSupSet CompleteLattice.toCompleteSemilatticeSup Nat.unpair	—	iSup_prod Function.Surjective.iSup_comp Nat.surjective_unpair

---

← Back to Index