range_mono — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem range_mono [Preorder β] (f : α → β) {g : α → β} (h : ∀ a, f a ≤ g a) (hbdd : BddBelow (range f)) :
    BddBelow (range g) :=
  BddAbove.range_mono (β := βᵒᵈ) f h hbdd

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