ciSup_mono — Mathlib

English

If f ≤ g pointwise and g is bounded above, then iSup f ≤ iSup g.

Русский

Если f(x) ≤ g(x) для всех x и range g ограничено сверху, то iSup f ≤ iSup g.

LaTeX

$$BddAbove( range g ) ∧ (∀ x, f(x) ≤ g(x)) → iSup f ≤ iSup g$$

Lean4

/-- The indexed suprema of two functions are comparable if the functions are pointwise comparable -/
@[gcongr low]
theorem ciSup_mono {f g : ι → α} (B : BddAbove (range g)) (H : ∀ x, f x ≤ g x) : iSup f ≤ iSup g :=
  by
  cases isEmpty_or_nonempty ι
  · rw [iSup_of_empty', iSup_of_empty']
  · exact ciSup_le fun x => le_ciSup_of_le B x (H x)

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