directedOn_of_sup_mem — Mathlib

English

A set closed under taking sup is directed with respect to ≤.

Русский

Множество, замкнутое по верхней границе (sup), направлено относительно ≤.

LaTeX

$$$[DirectedOn\\ (· ≤ ·)\\ S] \\text{ from sup closure }$$$

Lean4

/-- A set stable by supremum is `≤`-directed. -/
theorem directedOn_of_sup_mem [SemilatticeSup α] {S : Set α} (H : ∀ ⦃i j⦄, i ∈ S → j ∈ S → i ⊔ j ∈ S) :
    DirectedOn (· ≤ ·) S := fun a ha b hb => ⟨a ⊔ b, H ha hb, le_sup_left, le_sup_right⟩

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