psigmaCongrRight_refl — Mathlib

English

The fiberwise identity fiber yields the identity on the whole PSigma: (psigmaCongrRight (λ a, Equiv.refl (β a))) = Equiv.refl (Σ' a, β a).

Русский

Фактически тождественный переход по каждому волокну приводит к тождественному отображению на всей зависимой сумме: (psigmaCongrRight (λ a, Equiv.refl (β a))) = Equiv.refl (Σ' a, β a).

LaTeX

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

Lean4

@[simp]
theorem psigmaCongrRight_refl {α} {β : α → Sort*} :
    (psigmaCongrRight fun a => Equiv.refl (β a)) = Equiv.refl (Σ' a, β a) :=
  rfl

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