nonempty_sum — Mathlib

English

Nonempty of Sum α β iff Nonempty α or Nonempty β.

Русский

Непусто суммы α ⊕ β тогда, когда непусто α или непусто β.

LaTeX

$$$\operatorname{Nonempty}(\mathrm{Sum}\, \alpha \beta) \iff \operatorname{Nonempty} \alpha \lor \operatorname{Nonempty} \beta$$$

Lean4

@[simp]
theorem nonempty_sum : Nonempty (α ⊕ β) ↔ Nonempty α ∨ Nonempty β :=
  Iff.intro
    (fun ⟨h⟩ ↦
      match h with
      | Sum.inl a => Or.inl ⟨a⟩
      | Sum.inr b => Or.inr ⟨b⟩)
    fun h ↦
    match h with
    | Or.inl ⟨a⟩ => ⟨Sum.inl a⟩
    | Or.inr ⟨b⟩ => ⟨Sum.inr b⟩

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