isLUB_biSup — Mathlib

English

For s ⊆ β and f: β → α in a complete lattice, IsLUB(f''s) with the supremum ⨆_{x∈s} f(x) holds; i.e., IsLUB (f '' s) (⨆ x ∈ s, f x).

Русский

Для множества s ⊆ β и функции f: β → α в полной решётке выполняется: IsLUB (f''s) (⨆ x∈s, f x).

LaTeX

$$$$ \operatorname{IsLUB}(f''s, \bigvee_{x\in s} f(x)) $$$$

Lean4

theorem isLUB_biSup {s : Set β} {f : β → α} : IsLUB (f '' s) (⨆ x ∈ s, f x) := by
  simpa only [range_comp, Subtype.range_coe, iSup_subtype'] using @isLUB_iSup α s _ (f ∘ fun x => (x : β))

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