Denumerable

📁 Source: Mathlib/Logic/Denumerable.lean

Statistics

Metric	Count
Definitions Denumerable, equiv₂, eqv, int, mk', nat, ofEncodableOfInfinite, ofEquiv, ofNat, option, pair, plift, pnat, prod, sigma, sum, toEncodable, ulift, denumerable, ofNat, succ	21
Theorems decode_eq_ofNat, decode_inv, decode_isSome, encode_ofNat, instInfinite, ofEquiv_ofNat, ofNat_encode, ofNat_nat, ofNat_of_decode, prod_nat_ofNat, prod_ofNat_val, sigma_ofNat_val, coe_comp_ofNat_range, exists_succ, le_succ_of_forall_lt_le, lt_succ_iff_le, lt_succ_self, ofNat_range, ofNat_surjective, succ_le_of_lt, nonempty_denumerable, nonempty_denumerable_iff, nonempty_equiv_of_countable	23
Total	44

Denumerable

Definitions

Name	Category	Theorems
equiv₂ 📖	CompOp	1 math math: Computable.equiv₂
eqv 📖	CompOp	1 math math: Computable.eqv
int 📖	CompOp	—
mk' 📖	CompOp	—
nat 📖	CompOp	99 math math: Primrec.nat_double, Computable.encode_iff, Computable.list_getElem?, Primrec.nat_add, Computable.encode, not_primrec_ack_self, Primrec.list_length, Primrec.list_findIdx₁, Nat.Partrec'.to_part, Primrec.list_getElem?₁, Computable.ofNat, Primrec₂.unpaired, Nat.Partrec.Code.primrec_pappAck, not_primrec₂_ack, Computable.decode, Nat.Partrec.Code.instCountableSubtypePFunPartrec, Primrec.list_idxOf, Primrec₂.encode_iff, Computable.bind_decode_iff, Primrec.nat_lt, Primrec₂.unpaired', Computable.map_decode_iff, ManyOneDegree.liftOn₂_eq, Nat.Primrec'.prim_iff₂, Primrec.nat_mul, Nat.Partrec.Code.instCountableSubtypeForallComputable, Nat.Primrec'.prim_iff, ManyOneDegree.liftOn_eq, manyOneReducible_toNat_toNat, Partrec₂.unpaired', Nat.Partrec.Code.primrec_evaln, Primrec.nat_le, Computable.nat_strong_rec, Primrec.fin_val, Primrec.decode₂, Partrec.nat_iff, Primrec.unpair, Primrec.list_range, Computable.eqv, Computable.unpair, Primrec.nat_div, Computable.list_length, Primrec.encode_iff, Primrec.fin_val_iff, Nat.Partrec'.part_iff, Primrec.decode, Nat.Partrec.Code.primrec₂_curry, Nat.Partrec.Code.eval_part, Nat.Partrec'.part_iff₂, Primrec.nat_sub, Primrec.nat_max, Nat.Partrec'.vec_iff, Primrec.nat_iff, manyOneReducible_toNat, Primrec₂.ofNat_iff, Nat.Primrec'.to_prim, Primrec.nat_double_succ, Primrec.succ, Primrec.nat_min, Computable.vector_length, Primrec.encdec, Nat.Primrec'.prim_iff₁, manyOneEquiv_toNat, Primrec.vector_length, Primrec.list_getElem?, Primrec.bind_decode_iff, Primrec₂.nat_iff', Primcodable.mem_range_encode, Computable.succ, Primrec₂.natPair, Nat.Primrec'.vec_iff, Primrec.map_decode_iff, Primrec.list_getD, toNat_manyOneReducible, Computable.nat_div2, Nat.Partrec.Code.smn, Primrec.nat_div2, Partrec.map_encode_iff, Primrec.list_idxOf₁, Partrec₂.unpaired, ofNat_nat, Primrec.nat_strong_rec, Primrec.list_getI, Computable.pred, Primrec.ofNat_iff, Primrec.nat_sqrt, prod_nat_ofNat, Nat.Partrec.Code.primrec_const, computable₂_ack, Computable.nat_bodd, Nat.Partrec'.rfindOpt, Primrec.ofNat, Nat.Partrec'.part_iff₁, toNat_manyOneEquiv, Primrec.pred, Primrec.encode, Primrec.nat_bodd, Primrec.nat_mod, Primrec.list_findIdx
ofEncodableOfInfinite 📖	CompOp	—
ofEquiv 📖	CompOp	1 math math: ofEquiv_ofNat
ofNat 📖	CompOp	18 math math: prod_ofNat_val, Computable.ofNat, ofNat_encode, list_ofNat_succ, encode_ofNat, list_ofNat_zero, ofEquiv_ofNat, decode_eq_ofNat, sigma_ofNat_val, Primrec₂.ofNat_iff, Primrec.dom_denumerable, ofNat_of_decode, Nat.Partrec.Code.ofNatCode_eq, ofNat_nat, Primrec.ofNat_iff, prod_nat_ofNat, Nat.Partrec'.rfindOpt, Primrec.ofNat
option 📖	CompOp	1 math math: Nat.Partrec'.rfindOpt
pair 📖	CompOp	—
plift 📖	CompOp	—
pnat 📖	CompOp	—
prod 📖	CompOp	2 math math: prod_ofNat_val, prod_nat_ofNat
sigma 📖	CompOp	1 math math: sigma_ofNat_val
sum 📖	CompOp	—
toEncodable 📖	CompOp	7 math math: ofNat_encode, denumerable_list_aux, encode_ofNat, decode_eq_ofNat, decode_isSome, ProbabilityTheory.Kernel.isSFiniteKernel_sum_of_denumerable, decode_inv
ulift 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
decode_eq_ofNat 📖	mathematical	—	Encodable.decode toEncodable ofNat	—	decode_isSome
decode_inv 📖	mathematical	—	Encodable.decode toEncodable Encodable.encode	—	—
decode_isSome 📖	mathematical	—	Encodable.decode toEncodable	—	decode_inv
encode_ofNat 📖	mathematical	—	Encodable.encode toEncodable ofNat	—	decode_inv ofNat_of_decode
instInfinite 📖	mathematical	—	Infinite	—	Infinite.of_surjective instInfiniteNat Equiv.surjective
ofEquiv_ofNat 📖	mathematical	—	ofNat ofEquiv DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Equiv.symm	—	ofNat_of_decode Encodable.decode_ofEquiv decode_eq_ofNat
ofNat_encode 📖	mathematical	—	ofNat Encodable.encode toEncodable	—	ofNat_of_decode Encodable.encodek
ofNat_nat 📖	mathematical	—	ofNat nat	—	—
ofNat_of_decode 📖	mathematical	Encodable.decode toEncodable	ofNat	—	decode_eq_ofNat
prod_nat_ofNat 📖	mathematical	—	ofNat prod nat Nat.unpair	—	ofEquiv_ofNat sigma_ofNat_val
prod_ofNat_val 📖	mathematical	—	ofNat prod Nat.unpair	—	ofEquiv_ofNat sigma_ofNat_val
sigma_ofNat_val 📖	mathematical	—	ofNat sigma Nat.unpair	—	decode_eq_ofNat Encodable.decode_sigma_val Option.bind_congr'

Nat.Subtype

Definitions

Name	Category	Theorems
denumerable 📖	CompOp	—
ofNat 📖	CompOp	6 math math: Nat.orderEmbeddingOfSet_apply, Nat.coe_orderEmbeddingOfSet, orderIsoOfNat_apply, ofNat_range, coe_comp_ofNat_range, ofNat_surjective
succ 📖	CompOp	4 math math: lt_succ_iff_le, lt_succ_self, succ_le_of_lt, le_succ_of_forall_lt_le

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_comp_ofNat_range 📖	mathematical	—	Set.range Set.Elem Set Set.instMembership ofNat	—	Set.range_comp ofNat_range Set.image_univ Subtype.range_coe
exists_succ 📖	mathematical	—	Set Set.instMembership	—	lt_of_not_ge Fintype.false
le_succ_of_forall_lt_le 📖	mathematical	Set.Elem Set Set.instMembership	succ	—	exists_succ le_of_not_gt LE.le.not_gt Nat.find_spec
lt_succ_iff_le 📖	mathematical	—	Set.Elem Set Set.instMembership succ	—	le_of_not_gt not_le_of_gt succ_le_of_lt lt_of_le_of_lt lt_succ_self
lt_succ_self 📖	mathematical	—	Set.Elem Set Set.instMembership succ	—	exists_succ
ofNat_range 📖	mathematical	—	Set.range Set.Elem ofNat Set.univ	—	Function.Surjective.range_eq ofNat_surjective
ofNat_surjective 📖	mathematical	—	Set.Elem ofNat	—	le_antisymm bot_le Nontrivial.to_nonempty Infinite.instNontrivial le_of_not_gt List.maximum_eq_bot List.maximum_mem succ_le_of_lt le_succ_of_forall_lt_le List.le_maximum_of_mem
succ_le_of_lt 📖	mathematical	Set.Elem Set Set.instMembership	succ	—	exists_succ Nat.find_min'

(root)

Definitions

Name	Category	Theorems
Denumerable 📖	CompData	4 math math: Set.countable_infinite_iff_nonempty_denumerable, nonempty_denumerable_iff, Cardinal.denumerable_iff, nonempty_denumerable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
nonempty_denumerable 📖	mathematical	—	Denumerable	—	Nonempty.map nonempty_encodable
nonempty_denumerable_iff 📖	mathematical	—	Denumerable Countable Infinite	—	Encodable.countable Denumerable.instInfinite nonempty_denumerable
nonempty_equiv_of_countable 📖	mathematical	—	Equiv	—	nonempty_denumerable

---

← Back to Index