dirSupClosed_iff_forall_sSup — Mathlib

English

In a complete lattice, DirSupInacc s is characterized by sSup(d) ∈ s for all directed nonempty d contained in s.

Русский

В полной решётке DirSupInacc s характеризуется тем, что для каждого направленного ненулевого d, вложенного в s, выполняется sSup(d) ∈ s.

LaTeX

$$$\\text{DirSupInacc}(s) \\iff \\forall d\\ (d\\neq\\emptyset)\\to DirectedOn(\\le) d \\to d \\subseteq s \\to sSup(d) \\in s$$$

Lean4

theorem dirSupClosed_iff_forall_sSup : DirSupClosed s ↔ ∀ ⦃d⦄, d.Nonempty → DirectedOn (· ≤ ·) d → d ⊆ s → sSup d ∈ s :=
  by simp [DirSupClosed, isLUB_iff_sSup_eq]

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