English
Dual of above: range is bounded below iff the ranges of the fst and snd projections are bounded below.
Русский
Двойственность: диапазон ограничен снизу тогда и только тогда, когда проекции fst и snd ограничены снизу.
LaTeX
$$$ \\IsBoundedBelow(\\mathrm{range}\\ F) \\iff \\IsBoundedBelow(\\mathrm{range}(Prod.fst \\circ F)) \\land \\IsBoundedBelow(\\mathrm{range}(Prod.snd \\circ F)) $$$
Lean4
theorem bddBelow_range_prod {F : ι → α × β} :
BddBelow (range F) ↔ BddBelow (range <| Prod.fst ∘ F) ∧ BddBelow (range <| Prod.snd ∘ F) :=
bddAbove_range_prod (α := αᵒᵈ) (β := βᵒᵈ)