piCongrLeft_refl — Mathlib

English

If e is the identity on α, then piCongrLeft P e is the identity on the function space ∀ a, P a.

Русский

Если e — тождественный отображение на α, то piCongrLeft P e является тождественным на пространстве функций ∀ a, P a.

LaTeX

$$$\\mathrm{piCongrLeft}\,P\\, (\\mathrm{Id}_{\\alpha}) = \\mathrm{Id}_{\\forall a, P a}.$$$

Lean4

@[simp]
theorem piCongrLeft_refl (P : α → Sort*) : piCongrLeft P (.refl α) = .refl (∀ a, P a) :=
  rfl

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