piCongrLeft'_refl — Mathlib

English

If the base equivalence is the identity, the induced equivalence on dependent function spaces is the identity: piCongrLeft' P (id).

Русский

Если базовая эквивалентность тождественна, полученная эквивалентность на пространстве зависимых функций тождественна: piCongrLeft' P (id).

LaTeX

$$$\pi\text{-}CongrLeft'(P, \mathrm{id}) = \mathrm{id}_{(\forall a, P(a))}.$$$

Lean4

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

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