sups — Mathlib

English

If s and t are nonempty finite sets in a semilattice, then the set of pairwise joins s ⊻ t is nonempty.

Русский

Если S и T непусты и являются конечными множествами в полуполе с операцией объединения, то множество попарных наибольших элементов S ⊻ T непусто.

LaTeX

$$$ s \neq \varnothing \;\land\ t \neq \varnothing \;\Rightarrow\; (s \oplus t) \neq \varnothing $$$

Lean4

@[aesop safe apply (rule_sets := [finsetNonempty])]
protected theorem sups : s.Nonempty → t.Nonempty → (s ⊻ t).Nonempty :=
  Nonempty.image₂

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