bddAbove_range_pi — Mathlib

English

Is bounded above of a range of F corresponds to bounds of ranges of fst and a-projection under F.

Русский

Для диапазона F ограниченность сверху соответствует границам диапазонов проекции fst и проекции на a.

LaTeX

$$$ \\IsBoundedAbove(\\mathrm{range} F) \\iff \\forall a, \\IsBoundedAbove(\\mathrm{range}(\\lambda i, F i a)) $$$

Lean4

theorem bddAbove_range_pi {F : ι → ∀ a, π a} : BddAbove (range F) ↔ ∀ a, BddAbove (range fun i ↦ F i a) :=
  by
  simp only [bddAbove_pi, ← range_comp]
  rfl

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