iInf₂_mono' — Mathlib

English

Let f : ∀ i, κ i → α and g : ∀ i', κ' i' → α be such that for all i', j' we have f i' j' ≤ g i j. Then ⨅ i (⨅ j, f i j) ≤ ⨅ i (⨅ j, g i j).

Русский

Пусть f и g как выше, что для всех i', j' выполняется f(i', j') ≤ g(i, j). Тогда ⨅_{i,j} f(i,j) ≤ ⨅_{i,j} g(i,j).

LaTeX

$$$\\\\forall i'\\\\forall j', f(i' , j') \\\\le g(i, j) \\\\Rightarrow \\\\bigwedge_{i}\\\\bigwedge_{j} f(i,j) \\\\le \\\\bigwedge_{i}\\\\bigwedge_{j} g(i,j)$$$

Lean4

theorem iInf₂_mono' {f : ∀ i, κ i → α} {g : ∀ i', κ' i' → α} (h : ∀ i j, ∃ i' j', f i' j' ≤ g i j) :
    ⨅ (i) (j), f i j ≤ ⨅ (i) (j), g i j :=
  le_iInf₂ fun i j =>
    let ⟨i', j', h⟩ := h i j
    iInf₂_le_of_le i' j' h

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