English
Let f : ∀ i, κ i → α and g : ∀ i', κ' i' → α be such that for all i,j there exist i', j' with f i j ≤ g i' j'. Then ⨆ i (⨆ j, f i j) ≤ ⨆ i (⨆ j, g i j).
Русский
Пусть f и g как выше так, что для всех i,j существуют i', j' с f(i,j) ≤ g(i', j'). Тогда ⨆_{i,j} f(i,j) ≤ ⨆_{i,j} g(i,j).
LaTeX
$$$\\\\forall i j, \\\\exists i' j', f(i,j) \\\\le g(i', j') \\\\Rightarrow \\\\bigvee_{i}\\\\bigvee_{j} f(i,j) \\\\le \\\\bigvee_{i}\\\\bigvee_{j} g(i,j)$$$
Lean4
theorem iSup₂_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 :=
iSup₂_le fun i j =>
let ⟨i', j', h⟩ := h i j
le_iSup₂_of_le i' j' h
