directedOn_of_inf_mem — Mathlib

English

A set stable under infimum is directed with respect to ≥.

Русский

Множество, сохранённое по инфимному, направлено относительно ≥.

LaTeX

$$$[SemilatticeInf α] \\ {S} \\to DirectedOn\\ (fun x1 x2 => GE.ge x1 x2) S$$$

Lean4

/-- A set stable by infimum is `≥`-directed. -/
theorem directedOn_of_inf_mem [SemilatticeInf α] {S : Set α} (H : ∀ ⦃i j⦄, i ∈ S → j ∈ S → i ⊓ j ∈ S) :
    DirectedOn (· ≥ ·) S :=
  directedOn_of_sup_mem (α := αᵒᵈ) H

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