isEmpty_psum — Mathlib

English

The sum PSum α β is empty if and only if both α and β are empty; equivalently IsEmpty (α ⊕' β) ↔ (IsEmpty α ∧ IsEmpty β).

Русский

Сумма PSumαβ пустая тогда и только тогда, когда оба α и β пусты; то есть IsEmpty (α ⊕' β) ↔ (IsEmpty α ∧ IsEmpty β).

LaTeX

$$$IsEmpty (\\alpha \\oplus' \\beta) \\iff (IsEmpty \\alpha \\land IsEmpty \\beta)$$$

Lean4

@[simp]
theorem isEmpty_psum {α β} : IsEmpty (α ⊕' β) ↔ IsEmpty α ∧ IsEmpty β := by
  simp only [← not_nonempty_iff, nonempty_psum, not_or]

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