disjSups_singleton — Mathlib

English

The disjSups of singleton sets equals a singleton of the join if disjoint, else empty.

Русский

ДисjointSups для синглтонов: либо получается один элемент a ⊔ b, если Disjoint a b, иначе пустое.

LaTeX

$$Eq (({a} disjSups {b})) (ite (Disjoint a b) {a ⊔ b} ∅)$$

Lean4

theorem disjSups_singleton : ({ a } ○ { b } : Finset α) = if Disjoint a b then {a ⊔ b} else ∅ := by
  split_ifs with h <;> simp [disjSups, filter_singleton, h]

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