sigmaCongrRight_refl — Mathlib

English

The right-congruence with identity fibers is the identity on the Sigma type: (sigmaCongrRight (λ a, Equiv.refl (β a))) = Equiv.refl (Σ a, β a).

Русский

Правое конгруэнтное отображение с тождественными волокнами равно тождественному отображению на сигма-типе.

LaTeX

$$$$(\sigmaCongrRight (\lambda a, Equiv.refl (\beta a))). = Equiv.refl (\Sigma a, \beta a).$$$$

Lean4

@[simp]
theorem sigmaCongrRight_refl {α} {β : α → Type*} :
    (sigmaCongrRight fun a => Equiv.refl (β a)) = Equiv.refl (Σ a, β a) :=
  rfl

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