homeoBot — Mathlib

English

The obvious bijection between (Π i, R_i) and (Πʳ i, [R_i, A_i]_[⊥]) is a homeomorphism.

Русский

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

LaTeX

$$homeoBot : (Π i, R_i) ≃ₜ (Πʳ i, [R_i, A_i]_[⊥])$$

Lean4

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

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