piCongr_symm_apply — Mathlib

English

Symmetry compatibility: the symm part of piCongr acts on f by composing with the fiber symmetries.

Русский

Симметрия сохраняется: симм-часть piCongr действует на f через композицию с симм-ом соответствующих волокон.

LaTeX

$$$\\big(h_1.\\piCongr h_2\\big).\\text{symm} f = f \\mapsto (a\\mapsto (h_2 a)^{-1}(f(h_1 a))).$$$

Lean4

@[simp]
theorem piCongr_symm_apply (f : ∀ b, Z b) : (h₁.piCongr h₂).symm f = fun a => (h₂ a).symm (f (h₁ a)) :=
  rfl

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