biSup_mem — Mathlib

English

Given a finite set t of indices, if every f(i) ∈ L for i ∈ t, then the biSup over i ∈ t of f(i) belongs to L.

Русский

Пусть t конечно; если для всех i ∈ t выполняется f(i) ∈ L, то biSup над i ∈ t of f(i) ∈ L.

LaTeX

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

Lean4

theorem biSup_mem {ι : Type*} {t : Set ι} {f : ι → α} (ht : t.Finite) (hf : ∀ i ∈ t, f i ∈ L) : ⨆ i ∈ t, f i ∈ L :=
  L.supClosed.biSup_mem ht bot_mem hf

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