bddBelow_range_prod — Mathlib

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 (α := αᵒᵈ) (β := βᵒᵈ)

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