English
If s and t are preconnected, then s × t is preconnected.
Русский
Если s и t предсвязны, то их произведение предсвязно.
LaTeX
$$$\\mathrm{IsPreconnected}(s) \\land \\mathrm{IsPreconnected}(t) \\Rightarrow \\mathrm{IsPreconnected}(s \\times t)$$$
Lean4
theorem prod [TopologicalSpace β] {s : Set α} {t : Set β} (hs : IsPreconnected s) (ht : IsPreconnected t) :
IsPreconnected (s ×ˢ t) := by
apply isPreconnected_of_forall_pair
rintro ⟨a₁, b₁⟩ ⟨ha₁, hb₁⟩ ⟨a₂, b₂⟩ ⟨ha₂, hb₂⟩
refine ⟨Prod.mk a₁ '' t ∪ flip Prod.mk b₂ '' s, ?_, .inl ⟨b₁, hb₁, rfl⟩, .inr ⟨a₂, ha₂, rfl⟩, ?_⟩
· rintro _ (⟨y, hy, rfl⟩ | ⟨x, hx, rfl⟩)
exacts [⟨ha₁, hy⟩, ⟨hx, hb₂⟩]
·
exact
(ht.image _ (by fun_prop)).union (a₁, b₂) ⟨b₂, hb₂, rfl⟩ ⟨a₁, ha₁, rfl⟩
(hs.image _ (Continuous.prodMk_left _).continuousOn)
