bddAbove_range_comp — Mathlib

English

If range f is bounded above, then for any g, range (g ∘ f) is bounded above.

Русский

Если диапазон f ограничен сверху, то для любой g диапазон (g ∘ f) ограничен сверху.

LaTeX

$$$BddAbove(\mathrm{range}(f)) \Rightarrow \forall g, BddAbove(\mathrm{range}(g \circ f))$$$

Lean4

theorem bddAbove_range_comp {ι : Type u} {f : ι → Cardinal.{v}} (hf : BddAbove (range f))
    (g : Cardinal.{v} → Cardinal.{max v w}) : BddAbove (range (g ∘ f)) :=
  by
  rw [range_comp]
  exact bddAbove_image g hf

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