coe_piCongr_symm — Mathlib

English

The coe version of piCongr' is a simple definitional equality expressing the forward transport formula.

Русский

Версия coe для piCongr' выражается по определению через прямой перенос.

LaTeX

$$$\\text{coe}_{\\pi\\text{Congr}'}(h_1,h_2)=\\lambda f,b. h_2(b)(f(h_1^{-1}(b))).$$$

Lean4

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

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