nonempty_psum — Mathlib

English

Nonempty of PSum α β iff Nonempty α or Nonempty β.

Русский

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

LaTeX

$$$\operatorname{Nonempty}(\alpha \oplus' \beta) \iff \operatorname{Nonempty} \alpha \lor \operatorname{Nonempty} \beta$$$

Lean4

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

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