prod — Mathlib

English

The product of subsets s and t is homeomorphic to their product s × t.

Русский

Произведение подмножеств s и t гомеоморфно их произведению s × t.

LaTeX

$$$ (s : Set X) \timesˢ (t : Set Y) \cong_{Top} s \times t. $$$

Lean4

/-- `s ×ˢ t` is homeomorphic to `s × t`. -/
@[simps!]
def prod (s : Set X) (t : Set Y) : ↥(s ×ˢ t) ≃ₜ s × t
    where
  toEquiv := Equiv.Set.prod s t
  continuous_toFun := (continuous_subtype_val.fst.subtype_mk _).prodMk (continuous_subtype_val.snd.subtype_mk _)
  continuous_invFun := (continuous_subtype_val.fst'.prodMk continuous_subtype_val.snd').subtype_mk _

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