sigmaCongrRight_symm — Mathlib

English

The sigma-congruence for Perm fiber equals the permuted fiber-congruence: (sigmaCongrRight F).symm = sigmaCongrRight (λ a, (F a).symm).

Русский

Сигма-конгруэнтность для перестановок по волокнам равна симметрии перестановки: (sigmaCongrRight F).symm = sigmaCongrRight (λ a, (F a).symm).

LaTeX

$$$$(\sigmaCongrRight F).\text{symm} = \sigmaCongrRight (\lambda a, (F a).symm).$$$$

Lean4

@[simp]
theorem sigmaCongrRight_symm {α} {β : α → Sort _} (F : ∀ a, Perm (β a)) :
    (sigmaCongrRight F).symm = sigmaCongrRight fun a => (F a).symm :=
  rfl

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