psigmaCongrRight_symm — Mathlib

English

The right-congruence map for a family F is symmetric: (psigmaCongrRight F).symm = psigmaCongrRight (λ a, (F a).symm).

Русский

Правое сопряжение семейства эквивалентностей симметрично: (psigmaCongrRight F).symm = psigmaCongrRight (λ a, (F a).symm).

LaTeX

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

Lean4

@[grind =]
theorem psigmaCongrRight_symm {α} {β₁ β₂ : α → Sort*} (F : ∀ a, β₁ a ≃ β₂ a) :
    (psigmaCongrRight F).symm = psigmaCongrRight fun a => (F a).symm :=
  rfl

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