sigmaCongrRight_refl — Mathlib

English

The reflexive fiberwise equivalence yields the reflexive sigma-congruence: (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 {α} {β : α → Sort _} :
    (sigmaCongrRight fun a => Equiv.refl (β a)) = Equiv.refl (Σ a, β a) :=
  rfl

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