piCongr'_symm_apply_symm_apply — Mathlib

English

For any f and b, applying the inverse πCongr' to f at h₁⁻¹(b) matches the right-hand fiber.

Русский

Для любого f и b применение сопряжённого наоборот к f в h₁⁻¹(b) соответствует правому волокну.

LaTeX

$$$(h_1.piCongr' h_2).symm\\ f\\ (h_1.symm\\ b) = (h_2\\ b).symm\\ (f\\ b).$$$

Lean4

@[simp]
theorem piCongr'_symm_apply_symm_apply (f : ∀ b, Z b) (b : β) :
    (h₁.piCongr' h₂).symm f (h₁.symm b) = (h₂ b).symm (f b) := by simp [piCongr', piCongr_apply_apply]

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