iSup_iInf_le_iInf_iSup — Mathlib

English

For any f: ι → ι' → α, we have sup_i inf_j f(i,j) ≤ inf_j sup_i f(i,j).

Русский

Для любой функции f: ι → ι' → α верно, что sup_i inf_j f(i,j) ≤ inf_j sup_i f(i,j).

LaTeX

$$$\\\\forall f : ι \\\\to ι' \\\\to α, \\\\bigvee_{i}\\\\bigwedge_{j} f(i,j) \\\\le \\\\bigwedge_{j}\\\\bigvee_{i} f(i,j)$$$

Lean4

theorem iSup_iInf_le_iInf_iSup (f : ι → ι' → α) : ⨆ i, ⨅ j, f i j ≤ ⨅ j, ⨆ i, f i j :=
  iSup_le fun i => iInf_mono fun j => le_iSup (fun i => f i j) i

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