homeoTop — Mathlib

English

The obvious bijection between (Π i, A_i) and the restricted product with ⊤ is a homeomorphism.

Русский

Естественная биекция между полным произведением и ограниченным произведением над ⊤ есть гомеоморфизм.

LaTeX

$$homeoTop : (Π i, A_i) ≃ₜ (Πʳ i, [R_i, A_i]_[⊤])$$

Lean4

/-- The obvious bijection between `Πʳ i, [R i, A i]_[⊤]` and `Π i, A i` is a homeomorphism. -/
def homeoTop : (Π i, A i) ≃ₜ (Πʳ i, [R i, A i]_[⊤])
    where
  toFun f := ⟨fun i ↦ f i, fun i ↦ (f i).2⟩
  invFun f i := ⟨f i, f.2 i⟩
  continuous_toFun :=
    continuous_rng_of_top.mpr <| continuous_pi fun i ↦ continuous_subtype_val.comp <| continuous_apply i
  continuous_invFun := continuous_pi fun i ↦ continuous_induced_rng.mpr <| continuous_eval i

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