range_mono — Mathlib

English

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

Русский

Если f не выше g по каждой точке и диапазон g ограничен сверху, то диапазон f ограничен сверху.

LaTeX

$$$ (\\forall a, f a \\le g a) \\rightarrow \\operatorname{BddAbove}(\\mathrm{range} g) \\rightarrow \\operatorname{BddAbove}(\\mathrm{range} f) $$$

Lean4

theorem range_mono [Preorder β] {f : α → β} (g : α → β) (h : ∀ a, f a ≤ g a) (hbdd : BddAbove (range g)) :
    BddAbove (range f) := by
  obtain ⟨C, hC⟩ := hbdd
  use C
  rintro - ⟨x, rfl⟩
  exact (h x).trans (hC <| mem_range_self x)

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