piCongrLeft_refl — Mathlib

English

If the index bijection is the identity, the uniform reindexing gives the identity on the product space.

Русский

Если биекция индексов является тождественной, то переиндексация даёт тождественный изоморфизм на произведение.

LaTeX

$$$\\pi\\text{CongrLeft}(\\mathrm{id}_{I}) = \\mathrm{id}_{\\prod_{i\\in I} X_i}$$$

Lean4

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

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