bddBelow_range_pi — Mathlib

English

Dual of above for bounded below ranges.

Русский

Двойственность: диапазон ограничен снизу по F эквивалентен ограниченности снизу проекций.

LaTeX

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

Lean4

theorem bddBelow_range_pi {F : ι → ∀ a, π a} : BddBelow (range F) ↔ ∀ a, BddBelow (range fun i ↦ F i a) :=
  bddAbove_range_pi (π := fun a ↦ (π a)ᵒᵈ)

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