sups_eq_empty — Mathlib

English

In a semilattice with join, s ⊻ t is empty if and only if s is empty or t is empty.

Русский

В полус\-решётке с операцией объединения по верхам A ⊻ B пусто тогда и только тогда, когда A пусто или B пусто.

LaTeX

$$$ (s \\veebar t) = \\emptyset \\iff s = \\emptyset \\lor t = \\emptyset $$$

Lean4

@[simp]
theorem sups_eq_empty : s ⊻ t = ∅ ↔ s = ∅ ∨ t = ∅ :=
  image2_eq_empty_iff

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