bddAbove_range_prod — Mathlib

English

For a function F : ι → α × β, the range is bounded above iff the ranges of the fst and snd projections are bounded above.

Русский

Для функции F : ι → α × β ограниченность сверху диапазона F эквивалентна ограниченности сверху диапазонов проекции fst и snd.

LaTeX

$$$ \\IsBoundedAbove(\\mathrm{range}\\ F) \\iff \\IsBoundedAbove(\\mathrm{range}(Prod.fst \\circ F)) \\land \\IsBoundedAbove(\\mathrm{range}(Prod.snd \\circ F)) $$$

Lean4

theorem bddAbove_range_prod {F : ι → α × β} :
    BddAbove (range F) ↔ BddAbove (range <| Prod.fst ∘ F) ∧ BddAbove (range <| Prod.snd ∘ F) := by
  simp only [bddAbove_prod, ← range_comp]

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