iSup_mem — Mathlib

English

If ι is finite and f(i) ∈ L for all i, then the supremum ⨆ i f(i) belongs to L.

Русский

Если индексный набор ι конечен и для каждого i из ι выполняется f(i) ∈ L, тогда их наивысшее верхнее сочетание принадлежит L.

LaTeX

$$$\\text{iSup\_mem} [Finite ι] (hf : \\forall i, f(i) \\in L) : \\bigvee_{i} f(i) \\in L$$$

Lean4

theorem iSup_mem [Finite ι] (hf : ∀ i, f i ∈ L) : ⨆ i, f i ∈ L :=
  L.supClosed.iSup_mem bot_mem hf

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