bddBelow_prod — Mathlib

English

Dual of above: a set s of pairs is bounded below iff its projections are bounded below.

Русский

Двойственность: множество пар ограничено снизу тогда и только тогда, когда проекции ограничены снизу.

LaTeX

$$$ \\IsBoundedBelow(s) \\iff \\IsBoundedBelow(\\mathrm{Set.image Prod.fst\\ s}) \\land \\IsBoundedBelow(\\mathrm{Set.image Prod.snd\\ s}) $$$

Lean4

theorem bddBelow_prod {s : Set (α × β)} : BddBelow s ↔ BddBelow (Prod.fst '' s) ∧ BddBelow (Prod.snd '' s) :=
  bddAbove_prod (α := αᵒᵈ) (β := βᵒᵈ)

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