prodCongr_refl_right — Mathlib

English

For any e : β₁ ≃ β₂, prodCongr e (Equiv.refl α₁) = prodCongrLeft (fun _ => e).

Русский

Для любого e : β₁ ≃ β₂ верно, что prodCongr e (Equiv.refl α₁) = prodCongrLeft (постоянная функция, возвращающая e).

LaTeX

$$$prodCongr\ e\ (Equiv.refl\ ;\alpha_1) = prodCongrLeft (fun\ _\ => e)$$$

Lean4

theorem prodCongr_refl_right (e : β₁ ≃ β₂) : prodCongr e (Equiv.refl α₁) = prodCongrLeft fun _ => e :=
  by
  ext ⟨a, b⟩ : 1
  simp

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