English
Let s be a subset of a semilattice with join ⊔. If s is closed under finite joins (suprema), then s is directed with respect to the order ≤: for any a,b ∈ s there exists c ∈ s such that a ≤ c and b ≤ c (take c = a ⊔ b).
Русский
Пусть s ⊆ α является подмножеством полупрямой с операцией объединения ⊔. Если s замкнуто относительно пары элементов под верхним объединением (sup), то для любых a,b ∈ s существует c ∈ s such that a ≤ c и b ≤ c (возьмём c = a ⊔ b).
LaTeX
$$$ (\\forall x \\in s)(\\forall y \\in s)(x \\sqcup y \\in s) \\Rightarrow (\\forall a \\in s)(\\forall b \\in s)(\\exists c \\in s\\, (a \\le c \\land b \\le c)) $$$
Lean4
theorem directedOn (hs : SupClosed s) : DirectedOn (· ≤ ·) s := fun _a ha _b hb ↦
⟨_, hs ha hb, le_sup_left, le_sup_right⟩
