map_iSup_le — Mathlib

English

Let f: α → β be antitone. Then f(iSup s) ≤ iInf (f∘s). In words, applying an antitone function to a supremum yields a value below the infimum of the function applied to the elements.

Русский

Пусть f: α → β антимонотонна. Тогда f(⊔ s) ≤ ⊓ f ∘ s.

LaTeX

$$$f(\\\\iSup s) \\\\le \\\\iInf (\\\\lambda i, f(s(i)))$$$

Lean4

theorem map_iSup_le [CompleteLattice β] {f : α → β} (hf : Antitone f) : f (iSup s) ≤ ⨅ i, f (s i) :=
  le_iInf fun _ => hf <| le_iSup _ _

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