iSup_le_iSup_of_partialSups_le_partialSups

English

If partialSups f ≤ partialSups g, then the supremum of f is ≤ the supremum of g.

Русский

Если partialSups f ≤ partialSups g, то sup f ≤ sup g.

LaTeX

$$$\text{If } partialSups f \le partialSups g,\; \bigvee_i f(i) \le \bigvee_i g(i)$$$

Lean4

theorem iSup_le_iSup_of_partialSups_le_partialSups {f g : ι → α} (h : partialSups f ≤ partialSups g) :
    ⨆ i, f i ≤ ⨆ i, g i := by
  rw [← iSup_partialSups_eq f, ← iSup_partialSups_eq g]
  exact iSup_mono h

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