dirSupInacc_iff_forall_sSup — Mathlib

English

For complete lattices, DirSupInacc s is equivalent to a property stated using sSup.

Русский

Для полных решёток DirSupInacc s эквивалентно свойству, сформулированному через sSup.

LaTeX

$$$\\text{DirSupInacc}(s) \\iff \\forall d\\ d.Nonempty \\to DirectedOn(\\le) d \\to d \\subseteq s \\Rightarrow sSup(d) \\in s$$$

Lean4

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

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