English
IsLUB of a subset of α×β is equivalent to IsLUBs of the projections onto α and β.
Русский
Наименьшее верхнее ограничение множества пар эквивалентно верхним ограничениям его проекций на каждую компоненту.
LaTeX
$$$ \\IsLUB s p \\iff (\\IsLUB (\\mathrm{Set.image Prod.fst s}) p.\\!\\text{fst}) \\land (\\IsLUB (\\mathrm{Set.image Prod.snd s}) p.\\!\\text{snd}) $$$
Lean4
theorem isLUB_prod {s : Set (α × β)} (p : α × β) : IsLUB s p ↔ IsLUB (Prod.fst '' s) p.1 ∧ IsLUB (Prod.snd '' s) p.2 :=
by
refine
⟨fun H =>
⟨⟨monotone_fst.mem_upperBounds_image H.1, fun a ha => ?_⟩,
⟨monotone_snd.mem_upperBounds_image H.1, fun a ha => ?_⟩⟩,
fun H => ⟨?_, ?_⟩⟩
· suffices h : (a, p.2) ∈ upperBounds s from (H.2 h).1
exact fun q hq => ⟨ha <| mem_image_of_mem _ hq, (H.1 hq).2⟩
· suffices h : (p.1, a) ∈ upperBounds s from (H.2 h).2
exact fun q hq => ⟨(H.1 hq).1, ha <| mem_image_of_mem _ hq⟩
· exact fun q hq => ⟨H.1.1 <| mem_image_of_mem _ hq, H.2.1 <| mem_image_of_mem _ hq⟩
· exact fun q hq => ⟨H.1.2 <| monotone_fst.mem_upperBounds_image hq, H.2.2 <| monotone_snd.mem_upperBounds_image hq⟩
