le_map_iSup₂ — Mathlib

English

Let f : α → β be monotone. Then for any s : i → κ i → α, ⨆ i ⨆ j f(s i j) ≤ f(⨆ i ⨆ j s i j).

Русский

Пусть f : α → β монотонна. Тогда для любого s: i → κ i → α выполняется ⨆_{i,j} f(s(i,j)) ≤ f(⨆_{i,j} s(i,j)).

LaTeX

$$[Monotone] f → (s : (i : ι) → κ i → α) → ∨ i ∨ j f(s i j) ≤ f(∨ i ∨ j s i j)$$

Lean4

theorem le_map_iSup₂ [CompleteLattice β] {f : α → β} (hf : Monotone f) (s : ∀ i, κ i → α) :
    ⨆ (i) (j), f (s i j) ≤ f (⨆ (i) (j), s i j) :=
  iSup₂_le fun _ _ => hf <| le_iSup₂ _ _

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