sum — Mathlib

English

If α and β are denumerable, then α ⊕ β is denumerable.

Русский

Если α и β денумерируемы, то их сумма α ⊕ β денумерируема.

LaTeX

$$$ \text{Denumerable}(\alpha \oplus \beta) $$$

Lean4

/-- If `α` and `β` are denumerable, then so is their sum. -/
instance sum : Denumerable (α ⊕ β) :=
  ⟨fun n => by
    suffices ∃ a ∈ @decodeSum α β _ _ n, encodeSum a = bit (bodd n) (div2 n) by simpa [bit_bodd_div2]
    simp only [decodeSum, boddDiv2_eq, decode_eq_ofNat, Option.map_some, Option.mem_def, Sum.exists]
    cases bodd n <;> simp [bit, encodeSum, Nat.two_mul]⟩

Похожие утверждения