English
A set s of pairs is bounded above iff its first projections and second projections are bounded above.
Русский
Множество пар ограничено сверху тогда и только тогда, когда проекции на первую и вторую компоненты ограничены сверху.
LaTeX
$$$ \\IsBoundedAbove(s) \\iff \\IsBoundedAbove(\\mathrm{Set.image Prod.fst\\ s}) \\land \\IsBoundedAbove(\\mathrm{Set.image Prod.snd\\ s}) $$$
Lean4
theorem bddAbove_prod {s : Set (α × β)} : BddAbove s ↔ BddAbove (Prod.fst '' s) ∧ BddAbove (Prod.snd '' s) :=
⟨fun ⟨p, hp⟩ ↦ ⟨⟨p.1, forall_mem_image.2 fun _q hq ↦ (hp hq).1⟩, ⟨p.2, forall_mem_image.2 fun _q hq ↦ (hp hq).2⟩⟩,
fun ⟨⟨x, hx⟩, ⟨y, hy⟩⟩ ↦ ⟨⟨x, y⟩, fun _p hp ↦ ⟨hx <| mem_image_of_mem _ hp, hy <| mem_image_of_mem _ hp⟩⟩⟩
