piCongrRight_refl — Mathlib

English

The piCongrRight construction with constant identity on each β(a) is the identity on the space ∀a,β(a).

Русский

Конструкция piCongrRight, применённая к константному тождественному отображению на каждом β(a), даёт тождество на всем пространстве ∀a, β(a).

LaTeX

$$$$ \\text{piCongrRight}\\left(\\lambda a. \\mathrm{refl}(\\beta(a))\\right) = \\mathrm{refl}(\\forall a, \\beta a). $$$$

Lean4

@[simp]
theorem piCongrRight_refl {β : α → Sort*} : piCongrRight (fun a ↦ .refl (β a)) = .refl (∀ a, β a) :=
  rfl

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