le_map_sInf — Mathlib

English

Let α, β be complete lattices and f: α → β antitone. For any set s ⊆ α, the supremum over a ∈ s of f(a) is bounded above by f of the infimum of s: ⨆ a∈s, f(a) ≤ f(sInf s).

Русский

Пусть α, β — полные решетки, f: α → β антимонотонна. Тогда максимальное значение по a∈s от f(a) не превосходит f от infimum(s): ⨆_{a∈s} f(a) ≤ f(sInf s).

LaTeX

$$$\\\\sup_{a\\\\in s} f(a) \\\\le f\\\\left(\\\\inf s\\\\right)$$

Lean4

theorem le_map_sInf [CompleteLattice β] {s : Set α} {f : α → β} (hf : Antitone f) : ⨆ a ∈ s, f a ≤ f (sInf s) :=
  hf.dual_left.le_map_sSup

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