English
The extreme points of the product set s × t are the product of extreme points: (s × t).extremePoints = s.extremePoints × t.extremePoints.
Русский
Крайние точки множества-образа s × t равны произведению крайних точек s и крайних точек t.
LaTeX
$$$(s \times t).extremePoints 𝕜 = s.extremePoints 𝕜 \times t.extremePoints 𝕜$$$
Lean4
@[simp]
theorem extremePoints_prod (s : Set E) (t : Set F) :
(s ×ˢ t).extremePoints 𝕜 = s.extremePoints 𝕜 ×ˢ t.extremePoints 𝕜 :=
by
ext ⟨x, y⟩
refine (and_congr_right fun hx ↦ ⟨fun h ↦ ⟨?_, ?_⟩, fun h ↦ ?_⟩).trans and_and_and_comm
· rintro x₁ hx₁ x₂ hx₂ ⟨a, b, ha, hb, hab, hx'⟩
ext
· exact h.1 hx₁.1 hx₂.1 ⟨a, b, ha, hb, hab, congrArg Prod.fst hx'⟩
· exact h.2 hx₁.2 hx₂.2 ⟨a, b, ha, hb, hab, congrArg Prod.snd hx'⟩
· rintro x₁ hx₁ x₂ hx₂ hx_fst
refine congrArg Prod.fst (h (mk_mem_prod hx₁ hx.2) (mk_mem_prod hx₂ hx.2) ?_)
rw [← Prod.image_mk_openSegment_left]
exact mem_image_of_mem _ hx_fst
· rintro x₁ hx₁ x₂ hx₂ hx_snd
refine congrArg Prod.snd (h (mk_mem_prod hx.1 hx₁) (mk_mem_prod hx.1 hx₂) ?_)
rw [← Prod.image_mk_openSegment_right]
exact mem_image_of_mem _ hx_snd
