piCongr_apply_apply — Mathlib

English

Applying piCongr to a function and then evaluating at the image of a under e recovers the fiber action: (h1.piCongr h2) f (h1 a) = h2 a (f a).

Русский

Применяя piCongr к функции и рассматривая значение на образе a под e, получаем действие на волокне: (h1.piCongr h2) f (h1 a) = h2 a (f a).

LaTeX

$$$h_1.piCongr h_2\\, f (h_1 a) = h_2\, a\\,(f\\, a).$$$

Lean4

@[simp]
theorem piCongr_apply_apply (f : ∀ a, W a) (a : α) : h₁.piCongr h₂ f (h₁ a) = h₂ a (f a) := by
  simp only [piCongr, piCongrRight, trans_apply, coe_fn_mk, piCongrLeft_apply_apply, Pi.map_apply]

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