Documentation

Mathlib.Logic.Encodable.Basic

Encodable types #

This file defines encodable (constructively countable) types as a typeclass. This is used to provide explicit encode/decode functions from and to ℕ, with the information that those functions are inverses of each other. The difference with Denumerable is that finite types are encodable. For infinite types, Encodable and Denumerable agree.

Main declarations #

Encodable α: States that there exists an explicit encoding function encode : α → ℕ with a partial inverse decode : ℕ → Option α.
decode₂: Version of decode that is equal to none outside of the range of encode. Useful as we do not require this in the definition of decode.
ulower α: Any encodable type has an equivalent type living in the lowest universe, namely a subtype of ℕ. ulower α finds it.

Implementation notes #

The point of asking for an explicit partial inverse decode : ℕ → Option α to encode : α → ℕ is to make the range of encode decidable even when the finiteness of α is not.

class Encodable (α : Type u_1) :

Type u_1

Encoding from Type α to ℕ
encode : α → ℕ
Decoding from ℕ to Option α
decode : ℕ → Option α
Invariant relationship between encoding and decoding
encodek : ∀ (a : α), decode (encode a) = some a

Constructively countable type. Made from an explicit injection encode : α → ℕ and a partial inverse decode : ℕ → Option α. Note that finite types are countable. See Denumerable if you wish to enforce infiniteness.

Instances

theorem Encodable.encode_injective {α : Type u_1} [inst : Encodable α] :

Function.Injective Encodable.encode

@[simp]

theorem Encodable.encode_inj {α : Type u_1} [inst : Encodable α] {a : α} {b : α} :

Encodable.encode a = Encodable.encode b ↔ a = b

instance Encodable.countable {α : Type u_1} [inst : Encodable α] :

Equations

@Encodable.countable = @Encodable.countable.proof_1

theorem Encodable.surjective_decode_iget (α : Type u_1) [inst : Encodable α] [inst : Inhabited α] :

Function.Surjective fun n => Option.iget (Encodable.decode n)

def Encodable.decidableEqOfEncodable (α : Type u_1) [inst : Encodable α] :

An encodable type has decidable equality. Not set as an instance because this is usually not the best way to infer decidability.

Equations

One or more equations did not get rendered due to their size.

def Encodable.ofLeftInjection {α : Type u_1} {β : Type u_2} [inst : Encodable α] (f : β → α) (finv : α → Option β) (linv : ∀ (b : β), finv (f b) = some b) :

If α is encodable and there is an injection f : β → α, then β is encodable as well.

Equations

One or more equations did not get rendered due to their size.

def Encodable.ofLeftInverse {α : Type u_1} {β : Type u_2} [inst : Encodable α] (f : β → α) (finv : α → β) (linv : ∀ (b : β), finv (f b) = b) :

If α is encodable and f : β → α is invertible, then β is encodable as well.

Equations

Encodable.ofLeftInverse f finv linv = Encodable.ofLeftInjection f (some ∘ finv) (_ : ∀ (b : β), some (finv (f b)) = some b)

def Encodable.ofEquiv {β : Type u_1} (α : Type u_2) [inst : Encodable α] (e : β ≃ α) :

Encodability is preserved by equivalence.

Equations

Encodable.ofEquiv α e = Encodable.ofLeftInverse ↑e ↑(Equiv.symm e) (_ : Function.LeftInverse e.invFun e.toFun)

theorem Encodable.encode_ofEquiv {α : Type u_1} {β : Type u_2} [inst : Encodable α] (e : β ≃ α) (b : β) :

Encodable.encode b = Encodable.encode (↑e b)

theorem Encodable.decode_ofEquiv {α : Type u_1} {β : Type u_2} [inst : Encodable α] (e : β ≃ α) (n : ℕ) :

Encodable.decode n = Option.map (↑(Equiv.symm e)) (Encodable.decode n)

instance Encodable.Nat.encodable :

Equations

Encodable.Nat.encodable = { encode := id, decode := some, encodek := Encodable.Nat.encodable.proof_1 }

@[simp]

theorem Encodable.encode_nat (n : ℕ) :

Encodable.encode n = n

@[simp]

theorem Encodable.decode_nat (n : ℕ) :

Encodable.decode n = some n

instance Encodable.IsEmpty.toEncodable {α : Type u_1} [inst : IsEmpty α] :

Equations

Encodable.IsEmpty.toEncodable = { encode := fun a => isEmptyElim a, decode := fun x => none, encodek := (_ : ∀ (a : α), (fun x => none) ((fun a => isEmptyElim a) a) = some a) }

instance Encodable.PUnit.encodable :

Encodable PUnit

Equations

Encodable.PUnit.encodable = { encode := fun x => 0, decode := fun n => Nat.casesOn n (some PUnit.unit) fun x => none, encodek := Encodable.PUnit.encodable.proof_1 }

@[simp]

theorem Encodable.encode_star :

Encodable.encode PUnit.unit = 0

@[simp]

theorem Encodable.decode_unit_zero :

Encodable.decode 0 = some PUnit.unit

@[simp]

theorem Encodable.decode_unit_succ (n : ℕ) :

Encodable.decode (Nat.succ n) = none

instance Option.encodable {α : Type u_1} [h : Encodable α] :

Encodable (Option α)

If α is encodable, then so is Option α.

Equations

One or more equations did not get rendered due to their size.

@[simp]

theorem Encodable.encode_none {α : Type u_1} [inst : Encodable α] :

Encodable.encode none = 0

@[simp]

theorem Encodable.encode_some {α : Type u_1} [inst : Encodable α] (a : α) :

Encodable.encode (some a) = Nat.succ (Encodable.encode a)

@[simp]

theorem Encodable.decode_option_zero {α : Type u_1} [inst : Encodable α] :

Encodable.decode 0 = some none

@[simp]

theorem Encodable.decode_option_succ {α : Type u_1} [inst : Encodable α] (n : ℕ) :

Encodable.decode (Nat.succ n) = Option.map some (Encodable.decode n)

def Encodable.decode₂ (α : Type u_1) [inst : Encodable α] (n : ℕ) :

Failsafe variant of decode. decode₂ α n returns the preimage of n under encode if it exists, and returns none if it doesn't. This requirement could be imposed directly on decode but is not to help make the definition easier to use.

Equations

Encodable.decode₂ α n = Option.bind (Encodable.decode n) (Option.guard fun a => Encodable.encode a = n)

theorem Encodable.mem_decode₂' {α : Type u_1} [inst : Encodable α] {n : ℕ} {a : α} :

a ∈ Encodable.decode₂ α n ↔ a ∈ Encodable.decode n ∧ Encodable.encode a = n

theorem Encodable.mem_decode₂ {α : Type u_1} [inst : Encodable α] {n : ℕ} {a : α} :

a ∈ Encodable.decode₂ α n ↔ Encodable.encode a = n

theorem Encodable.decode₂_eq_some {α : Type u_1} [inst : Encodable α] {n : ℕ} {a : α} :

Encodable.decode₂ α n = some a ↔ Encodable.encode a = n

@[simp]

theorem Encodable.decode₂_encode {α : Type u_1} [inst : Encodable α] (a : α) :

Encodable.decode₂ α (Encodable.encode a) = some a

theorem Encodable.decode₂_ne_none_iff {α : Type u_1} [inst : Encodable α] {n : ℕ} :

Encodable.decode₂ α n ≠ none ↔ n ∈ Set.range Encodable.encode

theorem Encodable.decode₂_is_partial_inv {α : Type u_1} [inst : Encodable α] :

Function.IsPartialInv Encodable.encode (Encodable.decode₂ α)

theorem Encodable.decode₂_inj {α : Type u_1} [inst : Encodable α] {n : ℕ} {a₁ : α} {a₂ : α} (h₁ : a₁ ∈ Encodable.decode₂ α n) (h₂ : a₂ ∈ Encodable.decode₂ α n) :

a₁ = a₂

theorem Encodable.encodek₂ {α : Type u_1} [inst : Encodable α] (a : α) :

Encodable.decode₂ α (Encodable.encode a) = some a

def Encodable.decidableRangeEncode (α : Type u_1) [inst : Encodable α] :

DecidablePred fun x => x ∈ Set.range Encodable.encode

The encoding function has decidable range.

Equations

One or more equations did not get rendered due to their size.

def Encodable.equivRangeEncode (α : Type u_1) [inst : Encodable α] :

α ≃ ↑(Set.range Encodable.encode)

An encodable type is equivalent to the range of its encoding function.

Equations

One or more equations did not get rendered due to their size.

def Encodable.Unique.encodable {α : Type u_1} [inst : Unique α] :

A type with unique element is encodable. This is not an instance to avoid diamonds.

Equations

Encodable.Unique.encodable = { encode := fun x => 0, decode := fun x => some default, encodek := (_ : ∀ (a : α), (fun x => some default) ((fun x => 0) a) = some a) }

def Encodable.encodeSum {α : Type u_1} {β : Type u_2} [inst : Encodable α] [inst : Encodable β] :

α ⊕ β → ℕ

Explicit encoding function for the sum of two encodable types.

Equations

Encodable.encodeSum x = match x with | Sum.inl a => 2 * Encodable.encode a | Sum.inr b => 2 * Encodable.encode b + 1

def Encodable.decodeSum {α : Type u_1} {β : Type u_2} [inst : Encodable α] [inst : Encodable β] (n : ℕ) :

Option (α ⊕ β)

Explicit decoding function for the sum of two encodable types.

Equations

Encodable.decodeSum n = match Nat.boddDiv2 n with | (false, m) => Option.map Sum.inl (Encodable.decode m) | (fst, m) => Option.map Sum.inr (Encodable.decode m)

instance Encodable.Sum.encodable {α : Type u_1} {β : Type u_2} [inst : Encodable α] [inst : Encodable β] :

Encodable (α ⊕ β)

If α and β are encodable, then so is their sum.

Equations

Encodable.Sum.encodable = { encode := Encodable.encodeSum, decode := Encodable.decodeSum, encodek := (_ : ∀ (s : α ⊕ β), Encodable.decodeSum (Encodable.encodeSum s) = some s) }

@[simp]

theorem Encodable.encode_inl {α : Type u_2} {β : Type u_1} [inst : Encodable α] [inst : Encodable β] (a : α) :

Encodable.encode (Sum.inl a) = 2 * Encodable.encode a

@[simp]

theorem Encodable.encode_inr {α : Type u_2} {β : Type u_1} [inst : Encodable α] [inst : Encodable β] (b : β) :

Encodable.encode (Sum.inr b) = 2 * Encodable.encode b + 1

@[simp]

theorem Encodable.decode_sum_val {α : Type u_1} {β : Type u_2} [inst : Encodable α] [inst : Encodable β] (n : ℕ) :

Encodable.decode n = Encodable.decodeSum n

instance Encodable.Bool.encodable :

Equations

Encodable.Bool.encodable = Encodable.ofEquiv (Unit ⊕ Unit) Equiv.boolEquivPUnitSumPUnit

@[simp]

theorem Encodable.encode_true :

Encodable.encode true = 1

@[simp]

theorem Encodable.encode_false :

Encodable.encode false = 0

@[simp]

theorem Encodable.decode_zero :

Encodable.decode 0 = some false

@[simp]

theorem Encodable.decode_one :

Encodable.decode 1 = some true

theorem Encodable.decode_ge_two (n : ℕ) (h : 2 ≤ n) :

Encodable.decode n = none

noncomputable instance Encodable.Prop.encodable :

Equations

Encodable.Prop.encodable = Encodable.ofEquiv Bool Equiv.propEquivBool

def Encodable.encodeSigma {α : Type u_1} {γ : α → Type u_2} [inst : Encodable α] [inst : (a : α) → Encodable (γ a)] :

Sigma γ → ℕ

Explicit encoding function for Sigma γ

Equations

Encodable.encodeSigma x = match x with | { fst := a, snd := b } => Nat.pair (Encodable.encode a) (Encodable.encode b)

def Encodable.decodeSigma {α : Type u_1} {γ : α → Type u_2} [inst : Encodable α] [inst : (a : α) → Encodable (γ a)] (n : ℕ) :

Option (Sigma γ)

Explicit decoding function for Sigma γ

Equations

Encodable.decodeSigma n = match Nat.unpair n with | (n₁, n₂) => Option.bind (Encodable.decode n₁) fun a => Option.map (Sigma.mk a) (Encodable.decode n₂)

instance Encodable.Sigma.encodable {α : Type u_1} {γ : α → Type u_2} [inst : Encodable α] [inst : (a : α) → Encodable (γ a)] :

Encodable (Sigma γ)

Equations

Encodable.Sigma.encodable = { encode := Encodable.encodeSigma, decode := Encodable.decodeSigma, encodek := (_ : ∀ (x : Sigma γ), Encodable.decodeSigma (Encodable.encodeSigma x) = some x) }

@[simp]

theorem Encodable.decode_sigma_val {α : Type u_1} {γ : α → Type u_2} [inst : Encodable α] [inst : (a : α) → Encodable (γ a)] (n : ℕ) :

Encodable.decode n = Option.bind (Encodable.decode (Nat.unpair n).fst) fun a => Option.map (Sigma.mk a) (Encodable.decode (Nat.unpair n).snd)

@[simp]

theorem Encodable.encode_sigma_val {α : Type u_2} {γ : α → Type u_1} [inst : Encodable α] [inst : (a : α) → Encodable (γ a)] (a : α) (b : γ a) :

Encodable.encode { fst := a, snd := b } = Nat.pair (Encodable.encode a) (Encodable.encode b)

instance Encodable.Prod.encodable {α : Type u_1} {β : Type u_2} [inst : Encodable α] [inst : Encodable β] :

Encodable (α × β)

If α and β are encodable, then so is their product.

Equations

Encodable.Prod.encodable = Encodable.ofEquiv ((_ : α) × β) (Equiv.symm (Equiv.sigmaEquivProd α β))

@[simp]

theorem Encodable.decode_prod_val {α : Type u_1} {β : Type u_2} [inst : Encodable β] [i : Encodable α] (n : ℕ) :

Encodable.decode n = Option.bind (Encodable.decode (Nat.unpair n).fst) fun a => Option.map (Prod.mk a) (Encodable.decode (Nat.unpair n).snd)

@[simp]

theorem Encodable.encode_prod_val {α : Type u_2} {β : Type u_1} [inst : Encodable α] [inst : Encodable β] (a : α) (b : β) :

Encodable.encode (a, b) = Nat.pair (Encodable.encode a) (Encodable.encode b)

def Encodable.encodeSubtype {α : Type u_1} {P : α → Prop} [encA : Encodable α] :

{ a // P a } → ℕ

Explicit encoding function for a decidable subtype of an encodable type

Equations

Encodable.encodeSubtype x = match x with | { val := v, property := property } => Encodable.encode v

def Encodable.decodeSubtype {α : Type u_1} {P : α → Prop} [encA : Encodable α] [decP : DecidablePred P] (v : ℕ) :

Option { a // P a }

Explicit decoding function for a decidable subtype of an encodable type

Equations

Encodable.decodeSubtype v = Option.bind (Encodable.decode v) fun a => if h : P a then some { val := a, property := h } else none

instance Encodable.Subtype.encodable {α : Type u_1} {P : α → Prop} [encA : Encodable α] [decP : DecidablePred P] :

Encodable { a // P a }

A decidable subtype of an encodable type is encodable.

Equations

One or more equations did not get rendered due to their size.

theorem Encodable.Subtype.encode_eq {α : Type u_1} {P : α → Prop} [encA : Encodable α] [decP : DecidablePred P] (a : Subtype P) :

Encodable.encode a = Encodable.encode ↑a

instance Encodable.Fin.encodable (n : ℕ) :

Encodable (Fin n)

Equations

Encodable.Fin.encodable n = Encodable.ofEquiv { i // i < n } Fin.equivSubtype

instance Encodable.Int.encodable :

Equations

Encodable.Int.encodable = Encodable.ofEquiv ℕ Equiv.intEquivNat

instance Encodable.PNat.encodable :

Equations

Encodable.PNat.encodable = Encodable.ofEquiv ℕ Equiv.pnatEquivNat

instance Encodable.ULift.encodable {α : Type u_1} [inst : Encodable α] :

Encodable (ULift α)

The lift of an encodable type is encodable.

Equations

Encodable.ULift.encodable = Encodable.ofEquiv α Equiv.ulift

instance Encodable.PLift.encodable {α : Type u_1} [inst : Encodable α] :

Encodable (PLift α)

The lift of an encodable type is encodable.

Equations

Encodable.PLift.encodable = Encodable.ofEquiv α Equiv.plift

noncomputable def Encodable.ofInj {α : Type u_1} {β : Type u_2} [inst : Encodable β] (f : α → β) (hf : Function.Injective f) :

If β is encodable and there is an injection f : α → β, then α is encodable as well.

Equations

Encodable.ofInj f hf = Encodable.ofLeftInjection f (Function.partialInv f) (_ : ∀ (x : α), Function.partialInv f (f x) = some x)

noncomputable def Encodable.ofCountable (α : Type u_1) [inst : Countable α] :

If α is countable, then it has a (non-canonical) Encodable structure.

Equations

Encodable.ofCountable α = Nonempty.some (_ : Nonempty (Encodable α))

@[simp]

theorem Encodable.nonempty_encodable {α : Type u_1} :

Nonempty (Encodable α) ↔ Countable α

theorem nonempty_encodable (α : Type u_1) [inst : Countable α] :

Nonempty (Encodable α)

See also nonempty_fintype, nonempty_denumerable.

instance instCountablePNat :

Equations

instCountablePNat = instCountablePNat.proof_1

def Ulower (α : Type u_1) [inst : Encodable α] :

ULower α : Type is an equivalent type in the lowest universe, given Encodable α.

Equations

Ulower α = ↑(Set.range Encodable.encode)

instance instDecidableEqUlower {α : Type u_1} [inst : Encodable α] :

DecidableEq (Ulower α)

Equations

instDecidableEqUlower = id (Encodable.decidableEqOfEncodable ↑(Set.range Encodable.encode))

instance instEncodableUlower {α : Type u_1} [inst : Encodable α] :

Encodable (Ulower α)

Equations

instEncodableUlower = id inferInstance

def Ulower.equiv (α : Type u_1) [inst : Encodable α] :

α ≃ Ulower α

The equivalence between the encodable type α and Ulower α : Type.

Equations

Ulower.equiv α = Encodable.equivRangeEncode α

def Ulower.down {α : Type u_1} [inst : Encodable α] (a : α) :

Lowers an a : α into Ulower α.

Equations

Ulower.down a = ↑(Ulower.equiv α) a

instance Ulower.instInhabitedUlower {α : Type u_1} [inst : Encodable α] [inst : Inhabited α] :

Inhabited (Ulower α)

Equations

Ulower.instInhabitedUlower = { default := Ulower.down default }

def Ulower.up {α : Type u_1} [inst : Encodable α] (a : Ulower α) :

α

Lifts an a : Ulower α into α.

Equations

Ulower.up a = ↑(Equiv.symm (Ulower.equiv α)) a

@[simp]

theorem Ulower.down_up {α : Type u_1} [inst : Encodable α] {a : Ulower α} :

Ulower.down (Ulower.up a) = a

@[simp]

theorem Ulower.up_down {α : Type u_1} [inst : Encodable α] {a : α} :

Ulower.up (Ulower.down a) = a

@[simp]

theorem Ulower.up_eq_up {α : Type u_1} [inst : Encodable α] {a : Ulower α} {b : Ulower α} :

Ulower.up a = Ulower.up b ↔ a = b

@[simp]

theorem Ulower.down_eq_down {α : Type u_1} [inst : Encodable α] {a : α} {b : α} :

Ulower.down a = Ulower.down b ↔ a = b

theorem Ulower.ext {α : Type u_1} [inst : Encodable α] {a : Ulower α} {b : Ulower α} :

Ulower.up a = Ulower.up b → a = b

def Encodable.chooseX {α : Type u_1} {p : α → Prop} [inst : Encodable α] [inst : DecidablePred p] (h : ∃ x, p x) :

{ a // p a }

Constructive choice function for a decidable subtype of an encodable type.

Equations

One or more equations did not get rendered due to their size.

def Encodable.choose {α : Type u_1} {p : α → Prop} [inst : Encodable α] [inst : DecidablePred p] (h : ∃ x, p x) :

α

Constructive choice function for a decidable predicate over an encodable type.

Equations

Encodable.choose h = ↑(Encodable.chooseX h)

theorem Encodable.choose_spec {α : Type u_1} {p : α → Prop} [inst : Encodable α] [inst : DecidablePred p] (h : ∃ x, p x) :

p (Encodable.choose h)

theorem Encodable.axiom_of_choice {α : Type u_1} {β : α → Type u_2} {R : (x : α) → β x → Prop} [inst : (a : α) → Encodable (β a)] [inst : (x : α) → (y : β x) → Decidable (R x y)] (H : ∀ (x : α), ∃ y, R x y) :

∃ f, (x : α) → R x (f x)

A constructive version of Classical.axiom_of_choice for Encodable types.

theorem Encodable.skolem {α : Type u_1} {β : α → Type u_2} {P : (x : α) → β x → Prop} [inst : (a : α) → Encodable (β a)] [inst : (x : α) → (y : β x) → Decidable (P x y)] :

(∀ (x : α), ∃ y, P x y) ↔ ∃ f, (x : α) → P x (f x)

A constructive version of Classical.skolem for Encodable types.

def Encodable.encode' (α : Type u_1) [inst : Encodable α] :

The encode function, viewed as an embedding.

Equations

Encodable.encode' α = { toFun := Encodable.encode, inj' := (_ : Function.Injective Encodable.encode) }

instance Encodable.instIsTransPreimageNatCoeEmbeddingToFunLikeInstEmbeddingLikeEmbeddingEncode'LeInstLENat {α : Type u_1} [inst : Encodable α] :

IsTrans α (↑(Encodable.encode' α) ⁻¹'o fun x x_1 => x ≤ x_1)

Equations

One or more equations did not get rendered due to their size.

instance Encodable.instIsAntisymmPreimageNatCoeEmbeddingToFunLikeInstEmbeddingLikeEmbeddingEncode'LeInstLENat {α : Type u_1} [inst : Encodable α] :

IsAntisymm α (↑(Encodable.encode' α) ⁻¹'o fun x x_1 => x ≤ x_1)

Equations

One or more equations did not get rendered due to their size.

instance Encodable.instIsTotalPreimageNatCoeEmbeddingToFunLikeInstEmbeddingLikeEmbeddingEncode'LeInstLENat {α : Type u_1} [inst : Encodable α] :

IsTotal α (↑(Encodable.encode' α) ⁻¹'o fun x x_1 => x ≤ x_1)

Equations

One or more equations did not get rendered due to their size.

noncomputable def Directed.sequence {α : Type u_1} {β : Type u_2} [inst : Encodable α] [inst : Inhabited α] {r : β → β → Prop} (f : α → β) (hf : Directed r f) :

ℕ → α

Given a Directed r function f : α → β defined on an encodable inhabited type, construct a noncomputable sequence such that r (f (x n)) (f (x (n + 1))) and r (f a) (f (x (encode a + 1)).

Equations

Directed.sequence f hf 0 = default
Directed.sequence f hf (Nat.succ n) = let p := Directed.sequence f hf n; match Encodable.decode n with | none => Classical.choose (hf p p) | some a => Classical.choose (hf p a)

theorem Directed.sequence_mono_nat {α : Type u_2} {β : Type u_1} [inst : Encodable α] [inst : Inhabited α] {r : β → β → Prop} {f : α → β} (hf : Directed r f) (n : ℕ) :

r (f (Directed.sequence f hf n)) (f (Directed.sequence f hf (n + 1)))

theorem Directed.rel_sequence {α : Type u_2} {β : Type u_1} [inst : Encodable α] [inst : Inhabited α] {r : β → β → Prop} {f : α → β} (hf : Directed r f) (a : α) :

r (f a) (f (Directed.sequence f hf (Encodable.encode a + 1)))

theorem Directed.sequence_mono {α : Type u_2} {β : Type u_1} [inst : Encodable α] [inst : Inhabited α] [inst : Preorder β] {f : α → β} (hf : Directed (fun x x_1 => x ≤ x_1) f) :

Monotone (f ∘ Directed.sequence f hf)

theorem Directed.le_sequence {α : Type u_2} {β : Type u_1} [inst : Encodable α] [inst : Inhabited α] [inst : Preorder β] {f : α → β} (hf : Directed (fun x x_1 => x ≤ x_1) f) (a : α) :

f a ≤ f (Directed.sequence f hf (Encodable.encode a + 1))

def Quotient.rep {α : Type u_1} {s : Setoid α} [inst : DecidableRel fun x x_1 => x ≈ x_1] [inst : Encodable α] (q : Quotient s) :

α

Representative of an equivalence class. This is a computable version of quot.out for a setoid on an encodable type.

Equations

Quotient.rep q = Encodable.choose (_ : ∃ a, Quotient.mk s a = q)

theorem Quotient.rep_spec {α : Type u_1} {s : Setoid α} [inst : DecidableRel fun x x_1 => x ≈ x_1] [inst : Encodable α] (q : Quotient s) :

Quotient.mk s (Quotient.rep q) = q

def encodableQuotient {α : Type u_1} {s : Setoid α} [inst : DecidableRel fun x x_1 => x ≈ x_1] [inst : Encodable α] :

Encodable (Quotient s)

The quotient of an encodable space by a decidable equivalence relation is encodable.

Equations

One or more equations did not get rendered due to their size.