piCongrLeft_refl — Mathlib

English

The piCongrLeft map with the identity bijection is the identity homeomorphism.

Русский

Гомеоморфизм piCongrLeft с тождественной биекцией является тождественным гомеоморфизмом.

LaTeX

$$$\text{piCongrLeft}({\mathrm{refl}}\ {\iota}) = {\mathrm{refl}}(\forall i, X_i).$$$

Lean4

@[simp]
theorem piCongrLeft_refl {ι : Type*} {X : ι → Type*} [∀ i, TopologicalSpace (X i)] :
    piCongrLeft (.refl ι) = .refl (∀ i, X i) :=
  rfl

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