Basic

📁 Source: Mathlib/Logic/Encodable/Basic.lean

Statistics

Metric	Count
Definitions encodable, sequence, encodable, chooseX, decidableEqOfEncodable, decidableRangeEncode, decode, decodeSigma, decodeSubtype, decodeSum, decode₂, encode, encode', encodeSigma, encodeSubtype, encodeSum, equivRangeEncode, ofCountable, ofEquiv, ofInj, ofLeftInjection, ofLeftInverse, encodable, encodable, toEncodable, encodable, encodable, encodable, encodable, encodable, encodable, rep, encodable, encodable, encodable, encodable, ULower, down, equiv, instInhabited, up, encodable, encodableQuotient, instDecidableEqULower, instEncodableULower	45
Theorems le_sequence, rel_sequence, sequence_anti, sequence_le, sequence_mono, sequence_mono_nat, encode_eq, axiom_of_choice, choose_spec, countable, decode_ge_two, decode_nat, decode_ofEquiv, decode_one, decode_option_succ, decode_option_zero, decode_prod_val, decode_sigma_val, decode_sum_val, decode_unit_succ, decode_unit_zero, decode_zero, decode₂_encode, decode₂_eq_some, decode₂_inj, decode₂_is_partial_inv, decode₂_ne_none_iff, encode_false, encode_inj, encode_injective, encode_inl, encode_inr, encode_nat, encode_none, encode_ofEquiv, encode_prod_val, encode_sigma_val, encode_some, encode_star, encode_true, encodek, encodek₂, instAntisymmPreimageNatCoeEmbeddingEncode'Le, instTotalPreimageNatCoeEmbeddingEncode'Le, mem_decode₂, mem_decode₂', nonempty_encodable, skolem, surjective_decode_getD, surjective_decode_iget, rep_spec, down_eq_down, down_up, ext, ext_iff, up_down, up_eq_up, instCountablePNat, nonempty_encodable	59
Total	104

Bool

Definitions

Name	Category	Theorems
encodable 📖	CompOp	5 math math: Encodable.decode_ge_two, Encodable.decode_zero, Encodable.encode_false, Encodable.encode_true, Encodable.decode_one

Directed

Definitions

Name	Category	Theorems
sequence 📖	CompOp	6 math math: rel_sequence, sequence_le, sequence_mono_nat, le_sequence, sequence_anti, sequence_mono

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
le_sequence 📖	mathematical	Directed Preorder.toLE	sequence Encodable.encode	—	rel_sequence
rel_sequence 📖	mathematical	Directed	sequence Encodable.encode	—	Encodable.encodek
sequence_anti 📖	mathematical	Directed Preorder.toLE	Antitone Nat.instPreorder sequence	—	antitone_nat_of_succ_le sequence_mono_nat
sequence_le 📖	mathematical	Directed Preorder.toLE	sequence Encodable.encode	—	rel_sequence
sequence_mono 📖	mathematical	Directed Preorder.toLE	Monotone Nat.instPreorder sequence	—	monotone_nat_of_le_succ sequence_mono_nat
sequence_mono_nat 📖	mathematical	Directed	sequence	—	—

Encodable

Definitions

Name	Category	Theorems
chooseX 📖	CompOp	—
decidableEqOfEncodable 📖	CompOp	—
decidableRangeEncode 📖	CompOp	—
decode 📖	CompOp	134 math math: decode_option_zero, Primrec.dom_bool, Primrec.vector_toList_iff, Primrec.nat_double, decode_sigma_val, Primrec.option_iget, Partrec.rfindOpt, Nat.Partrec.Code.primrec_pappAck_step, not_primrec_ack_self, Primrec.list_length, Primrec.list_findIdx₁, Nat.Partrec'.to_part, Primrec.listFilter, Primrec.list_getElem?₁, Primrec.snd, mem_decode₂', Primrec₂.unpaired, Nat.Partrec.Code.primrec_pappAck, decode_list_zero, Primrec.subtype_val_iff, Computable.decode, Partrec.sumCasesOn_right, decode_ge_two, Primrec.dom_finite, Primrec.option_getD_default, Nat.Partrec.Code.computable_recOn, Primrec₂.curry, Primrec.of_equiv_symm_iff, Primrec.dom_fintype, Primrec.option_isSome, Computable.bind_decode_iff, Primrec.vector_ofFn', Computable.map_decode_iff, Primrec.fst, Partrec.some, Nat.Primrec'.prim_iff, Primrec.of_equiv, primrecPred_iff_primrec_decide, Primrec.vector_tail, Nat.Partrec.Code.primrec_evaln, decode_zero, Nat.Partrec.Code.primrec_rfind', decode_option_succ, Primrec₂.uncurry, Partrec₂.comp, Primrec.fin_val, Primrec.decode₂, Primrec.fin_succ, Computable.ofOption, Primrec.const, decode_ofEquiv, Partrec.nat_iff, Primrec.unpair, Primrec.list_range, Denumerable.decode_eq_ofNat, Primrec.list_headI, Primrec.sumInl, decode_unit_zero, PrimrecPred.decide, Primrec.ulower_up, Computable.partrec, Primrec.encode_iff, Partrec.nat_casesOn_right, Primrec.fin_val_iff, Nat.Partrec'.part_iff, Primrec.decode, Partrec.const', decode_sum_val, Primrec.vector_toList, Primrec.nat_iff, Primrec.of_graph, Partrec.sumCasesOn_left, Nat.Primrec'.to_prim, encodek, Primrec.nat_double_succ, Primrec.succ, Primrec.dom_denumerable, Primrec.of_equiv_symm, Primrec.encdec, Primrec.list_flatten, Primrec.list_tail, Nat.Primrec'.prim_iff₁, Denumerable.decode_isSome, Primrec.option_some, Primrec.fin_curry, Partrec.none, Primrec.vector_length, Primrec.bind_decode_iff, Primrec₂.nat_iff', decode_prod_val, Nat.Primrec'.vec_iff, Primrec.option_some_iff, Partrec.bind_decode₂_iff, Primrec.map_decode_iff, Partrec.option_some_iff, Primrec.sumInr, Decidable.Partrec.const', Primrec.vector_get', Primrec.ulower_down, Primrec.optionToList, Primrec.nat_div2, Partrec.map_encode_iff, Primrec.list_idxOf₁, Partrec.optionCasesOn_right, Primrec.not, Denumerable.decode_inv, Partrec₂.unpaired, decode_nat, decode_unit_succ, Primrec.list_reverse, Primrec.of_equiv_iff, Primrec.ofNat_iff, Partrec.rfind, PrimrecPred.listFilter_listRange, Primrec.fin_curry₁, Primrec.list_head?, Primrec.nat_rec₁, Primrec.nat_sqrt, decode_list_succ, Primrec.subtype_val, Nat.Partrec.Code.primrec_const, Primrec.id, Primrec.ofNat, Nat.Partrec'.part_iff₁, surjective_decode_iget, Primcodable.prim, Primrec.vector_head, Primrec.pred, decode_one, Primrec.encode, Partrec.sumCasesOn, Primrec.nat_bodd, Primrec₂.nat_iff, surjective_decode_getD
decodeSigma 📖	CompOp	—
decodeSubtype 📖	CompOp	—
decodeSum 📖	CompOp	1 math math: decode_sum_val
decode₂ 📖	CompOp	16 math math: mem_decode₂, iSup_decode₂, iUnion_decode₂_cases, mem_decode₂', decode₂_encode, tsum_iSup_decode₂, tprod_iSup_decode₂, iUnion_decode₂, Primrec.decode₂, tsum_iUnion_decode₂, iUnion_decode₂_disjoint_on, Partrec.bind_decode₂_iff, tprod_iUnion_decode₂, encodek₂, decode₂_eq_some, decode₂_is_partial_inv
encode 📖	CompOp	160 math math: encode_nat, encode_inj, Nat.Partrec.Code.encode_lt_comp, Primrec.dom_bool, Subtype.encode_eq, Primrec.vector_toList_iff, Primrec.nat_double, Computable.encode_iff, encode_inl, Primrec.option_iget, tsum_geometric_encode_lt_top, PiCountable.min_dist_le_dist_pi, Nat.Primrec'.encode, Computable.encode, mem_decode₂, Directed.rel_sequence, Partrec.rfindOpt, Nat.Partrec.Code.primrec_pappAck_step, not_primrec_ack_self, Primrec.list_length, Primrec.list_findIdx₁, Metric.PiNatEmbed.edist_def, Nat.Partrec'.to_part, Primrec.listFilter, Primrec.list_getElem?₁, encode_list_nil, Denumerable.ofNat_encode, Primrec.snd, mem_decode₂', Primrec₂.unpaired, Nat.Partrec.Code.primrec_pappAck, Primrec.subtype_val_iff, length_le_encode, Partrec.sumCasesOn_right, PiCountable.min_edist_le_edist_pi, PiCountable.edist_eq_tsum, Metric.PiNatEmbed.dist_def, encode_sigma_val, Primrec.dom_finite, Primrec.option_getD_default, Nat.Partrec.Code.computable_recOn, Primrec₂.curry, Primrec.of_equiv_symm_iff, encode_inr, Primrec.dom_fintype, decode₂_encode, Nat.Partrec.Code.encodeCode_eq, Primrec₂.encode_iff, Primrec.option_isSome, Primrec.vector_ofFn', Primrec.fst, MeasureTheory.SimpleFunc.ennrealRatEmbed_encode, Partrec.some, encode_injective, Denumerable.encode_ofNat, Directed.sequence_le, Nat.Primrec'.prim_iff, Primrec.of_equiv, PiCountable.dist_summable, primrecPred_iff_primrec_decide, Primrec.vector_tail, Nat.Partrec.Code.primrec_evaln, Nat.Partrec.Code.primrec_rfind', Primrec₂.uncurry, Partrec₂.comp, encode_star, Primrec.fin_val, Primrec.decode₂, Primrec.fin_succ, Computable.ofOption, Primrec.const, Partrec.nat_iff, Primrec.unpair, Primrec.list_range, Primrec.list_headI, Primrec.sumInl, PrimrecPred.decide, Primrec.ulower_up, Computable.partrec, Primrec.encode_iff, Partrec.nat_casesOn_right, Primrec.fin_val_iff, Nat.Partrec'.part_iff, Primrec.decode, Partrec.const', Primrec.vector_toList, Primrec.nat_iff, Primrec.of_graph, Partrec.sumCasesOn_left, Nat.Primrec'.to_prim, encodek, Primrec.nat_double_succ, Primrec.succ, Primrec.dom_denumerable, encode_false, Primrec.of_equiv_symm, Primrec.encdec, Primrec.list_flatten, Primrec.list_tail, Nat.Primrec'.prim_iff₁, Primrec.option_some, Primrec.fin_curry, Partrec.none, Primrec.vector_length, Primcodable.mem_range_encode, Nat.Primrec'.vec_iff, Directed.le_sequence, Primrec.option_some_iff, Nat.Partrec.Code.encode_lt_rfind', Partrec.bind_decode₂_iff, Partrec.option_some_iff, Primrec.sumInr, Decidable.Partrec.const', Primrec.vector_get', Nat.Partrec.Code.encode_lt_pair, encode_prod_val, Primrec.ulower_down, ENNReal.tsum_geometric_two_encode_le_two, Primrec.optionToList, Primrec.nat_div2, Partrec.map_encode_iff, Primrec.list_idxOf₁, Order.sequenceOfCofinals.encode_mem, Partrec.optionCasesOn_right, Primrec.not, encode_none, decode₂_ne_none_iff, encodek₂, Denumerable.decode_inv, Partrec₂.unpaired, encode_true, encode_list_cons, Primrec.list_reverse, PiCountable.dist_eq_tsum, encode_ofEquiv, decode₂_eq_some, Primrec.of_equiv_iff, Primrec.ofNat_iff, Partrec.rfind, PrimrecPred.listFilter_listRange, Primrec.fin_curry₁, Primrec.list_head?, Primrec.nat_rec₁, Primrec.nat_sqrt, Nat.Partrec.Code.encode_lt_prec, Primrec.subtype_val, Nat.Partrec.Code.primrec_const, encode_some, Primrec.id, Primrec.ofNat, Nat.Partrec'.part_iff₁, Primcodable.prim, decode₂_is_partial_inv, Primrec.vector_head, Primrec.pred, summable_geometric_two_encode, Primrec.encode, Partrec.sumCasesOn, Primrec.nat_bodd, Primrec₂.nat_iff
encode' 📖	CompOp	2 math math: instTotalPreimageNatCoeEmbeddingEncode'Le, instAntisymmPreimageNatCoeEmbeddingEncode'Le
encodeSigma 📖	CompOp	—
encodeSubtype 📖	CompOp	—
encodeSum 📖	CompOp	—
equivRangeEncode 📖	CompOp	—
ofCountable 📖	CompOp	—
ofEquiv 📖	CompOp	2 math math: decode_ofEquiv, encode_ofEquiv
ofInj 📖	CompOp	—
ofLeftInjection 📖	CompOp	—
ofLeftInverse 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
axiom_of_choice 📖	—	—	—	—	choose_spec
choose_spec 📖	mathematical	—	choose	—	—
countable 📖	mathematical	—	Countable	—	encode_injective
decode_ge_two 📖	mathematical	—	decode Bool.encodable	—	ne_of_gt Nat.div2_val
decode_nat 📖	mathematical	—	decode Nat.encodable	—	—
decode_ofEquiv 📖	mathematical	—	decode ofEquiv DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Equiv.symm	—	—
decode_one 📖	mathematical	—	decode Bool.encodable	—	—
decode_option_succ 📖	mathematical	—	decode Option.encodable	—	—
decode_option_zero 📖	mathematical	—	decode Option.encodable	—	—
decode_prod_val 📖	mathematical	—	decode Prod.encodable Nat.unpair	—	decode_ofEquiv
decode_sigma_val 📖	mathematical	—	decode Sigma.encodable Nat.unpair	—	—
decode_sum_val 📖	mathematical	—	decode Sum.encodable decodeSum	—	—
decode_unit_succ 📖	mathematical	—	decode PUnit.encodable	—	—
decode_unit_zero 📖	mathematical	—	decode PUnit.encodable	—	—
decode_zero 📖	mathematical	—	decode Bool.encodable	—	—
decode₂_encode 📖	mathematical	—	decode₂ encode	—	—
decode₂_eq_some 📖	mathematical	—	decode₂ encode	—	mem_decode₂
decode₂_inj 📖	—	decode₂	—	—	encode_injective mem_decode₂
decode₂_is_partial_inv 📖	mathematical	—	Function.IsPartialInv encode decode₂	—	mem_decode₂
decode₂_ne_none_iff 📖	mathematical	—	Set Set.instMembership Set.range encode	—	—
encode_false 📖	mathematical	—	encode Bool.encodable	—	—
encode_inj 📖	mathematical	—	encode	—	encode_injective
encode_injective 📖	mathematical	—	encode	—	encodek
encode_inl 📖	mathematical	—	encode Sum.encodable	—	—
encode_inr 📖	mathematical	—	encode Sum.encodable	—	—
encode_nat 📖	mathematical	—	encode Nat.encodable	—	—
encode_none 📖	mathematical	—	encode Option.encodable	—	—
encode_ofEquiv 📖	mathematical	—	encode ofEquiv DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike	—	—
encode_prod_val 📖	mathematical	—	encode Prod.encodable Nat.pair	—	—
encode_sigma_val 📖	mathematical	—	encode Sigma.encodable Nat.pair	—	—
encode_some 📖	mathematical	—	encode Option.encodable	—	—
encode_star 📖	mathematical	—	encode PUnit.encodable	—	—
encode_true 📖	mathematical	—	encode Bool.encodable	—	—
encodek 📖	mathematical	—	decode encode	—	—
encodek₂ 📖	mathematical	—	decode₂ encode	—	mem_decode₂
instAntisymmPreimageNatCoeEmbeddingEncode'Le 📖	mathematical	—	Order.Preimage DFunLike.coe Function.Embedding Function.instFunLikeEmbedding encode'	—	RelEmbedding.antisymm
instTotalPreimageNatCoeEmbeddingEncode'Le 📖	mathematical	—	Order.Preimage DFunLike.coe Function.Embedding Function.instFunLikeEmbedding encode'	—	RelEmbedding.total LE.total
mem_decode₂ 📖	mathematical	—	decode₂ encode	—	mem_decode₂' encodek
mem_decode₂' 📖	mathematical	—	decode₂ decode encode	—	—
nonempty_encodable 📖	mathematical	—	Encodable Countable	—	countable
skolem 📖	—	—	—	—	axiom_of_choice
surjective_decode_getD 📖	mathematical	—	decode	—	encodek
surjective_decode_iget 📖	mathematical	—	decode	—	surjective_decode_getD

Encodable.Prod

Definitions

Name	Category	Theorems
encodable 📖	CompOp	2 math math: Encodable.decode_prod_val, Encodable.encode_prod_val

Encodable.Subtype

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
encode_eq 📖	mathematical	—	Encodable.encode Subtype.encodable	—	—

Fin

Definitions

Name	Category	Theorems
encodable 📖	CompOp	—

Int

Definitions

Name	Category	Theorems
encodable 📖	CompOp	—

IsEmpty

Definitions

Name	Category	Theorems
toEncodable 📖	CompOp	3 math math: FirstOrder.Language.empty.isFraisseLimit_of_countable_infinite, MeasureTheory.tendstoInDistribution_of_isEmpty, volume_euclideanSpace_eq_dirac

Nat

Definitions

Name	Category	Theorems
encodable 📖	CompOp	5 math math: Encodable.encode_nat, Metric.PiNatEmbed.continuous_distDenseSeq_inv, Primrec'.encode, FirstOrder.Language.empty.isFraisseLimit_of_countable_infinite, Encodable.decode_nat

Option

Definitions

Name	Category	Theorems
encodable 📖	CompOp	88 math math: Encodable.decode_option_zero, Primrec.dom_bool, Primrec.vector_toList_iff, Primrec.nat_double, Primrec.option_iget, Nat.Partrec.Code.primrec_pappAck_step, not_primrec_ack_self, Primrec.list_length, Primrec.list_findIdx₁, Primrec.listFilter, Primrec.list_getElem?₁, Primrec.snd, Primrec₂.unpaired, Nat.Partrec.Code.primrec_pappAck, Primrec.subtype_val_iff, Primrec.dom_finite, Primrec.option_getD_default, Primrec₂.curry, Primrec.of_equiv_symm_iff, Primrec.dom_fintype, Primrec.option_isSome, Primrec.vector_ofFn', Primrec.fst, Nat.Primrec'.prim_iff, Primrec.of_equiv, primrecPred_iff_primrec_decide, Primrec.vector_tail, Nat.Partrec.Code.primrec_evaln, Nat.Partrec.Code.primrec_rfind', Encodable.decode_option_succ, Primrec₂.uncurry, Primrec.fin_val, Primrec.decode₂, Primrec.fin_succ, Primrec.const, Primrec.unpair, Primrec.list_range, Primrec.list_headI, Primrec.sumInl, PrimrecPred.decide, Primrec.ulower_up, Primrec.encode_iff, Primrec.fin_val_iff, Primrec.decode, Primrec.vector_toList, Primrec.nat_iff, Primrec.of_graph, Nat.Primrec'.to_prim, Primrec.nat_double_succ, Primrec.succ, Primrec.dom_denumerable, Primrec.of_equiv_symm, Primrec.encdec, Primrec.list_flatten, Primrec.list_tail, Nat.Primrec'.prim_iff₁, Primrec.option_some, Primrec.fin_curry, Primrec.vector_length, Nat.Primrec'.vec_iff, Primrec.option_some_iff, Primrec.sumInr, Primrec.vector_get', Primrec.ulower_down, Primrec.optionToList, Primrec.nat_div2, Primrec.list_idxOf₁, Primrec.not, Encodable.encode_none, Primrec.list_reverse, Primrec.of_equiv_iff, Primrec.ofNat_iff, PrimrecPred.listFilter_listRange, Primrec.fin_curry₁, Primrec.list_head?, Primrec.nat_rec₁, Primrec.nat_sqrt, Primrec.subtype_val, Nat.Partrec.Code.primrec_const, Encodable.encode_some, Primrec.id, Primrec.ofNat, Primcodable.prim, Primrec.vector_head, Primrec.pred, Primrec.encode, Primrec.nat_bodd, Primrec₂.nat_iff

PLift

Definitions

Name	Category	Theorems
encodable 📖	CompOp	—

PNat

Definitions

Name	Category	Theorems
encodable 📖	CompOp	—

PUnit

Definitions

Name	Category	Theorems
encodable 📖	CompOp	3 math math: Encodable.encode_star, Encodable.decode_unit_zero, Encodable.decode_unit_succ

Prop

Definitions

Name	Category	Theorems
encodable 📖	CompOp	—

Quotient

Definitions

Name	Category	Theorems
rep 📖	CompOp	1 math math: rep_spec

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
rep_spec 📖	mathematical	—	rep	—	Encodable.choose_spec

Sigma

Definitions

Name	Category	Theorems
encodable 📖	CompOp	3 math math: Encodable.decode_sigma_val, FirstOrder.Language.empty.isFraisseLimit_of_countable_infinite, Encodable.encode_sigma_val

Subtype

Definitions

Name	Category	Theorems
encodable 📖	CompOp	1 math math: Encodable.Subtype.encode_eq

Sum

Definitions

Name	Category	Theorems
encodable 📖	CompOp	4 math math: Encodable.encode_inl, FirstOrder.Language.empty.isFraisseLimit_of_countable_infinite, Encodable.encode_inr, Encodable.decode_sum_val

ULift

Definitions

Name	Category	Theorems
encodable 📖	CompOp	—

ULower

Definitions

Name	Category	Theorems
down 📖	CompOp	4 math math: down_up, up_down, Primrec.ulower_down, down_eq_down
equiv 📖	CompOp	1 math math: down_computable
instInhabited 📖	CompOp	—
up 📖	CompOp	6 math math: down_up, up_down, Primrec.ulower_up, ext_iff, manyOneEquiv_up, up_eq_up

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
down_eq_down 📖	mathematical	—	down	—	Equiv.apply_eq_iff_eq
down_up 📖	mathematical	—	down up	—	Equiv.right_inv
ext 📖	—	up	—	—	up_eq_up
ext_iff 📖	mathematical	—	up	—	ext
up_down 📖	mathematical	—	up down	—	Equiv.symm_apply_apply
up_eq_up 📖	mathematical	—	up	—	Equiv.apply_eq_iff_eq

Unique

Definitions

Name	Category	Theorems
encodable 📖	CompOp	—

(root)

Definitions

Name	Category	Theorems
ULower 📖	CompOp	4 math math: ULower.down_computable, Primrec.ulower_up, Primrec.ulower_down, manyOneEquiv_up
encodableQuotient 📖	CompOp	—
instDecidableEqULower 📖	CompOp	—
instEncodableULower 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instCountablePNat 📖	mathematical	—	Countable PNat	—	Subtype.countable instCountableNat
nonempty_encodable 📖	mathematical	—	Encodable	—	—

---

← Back to Index