piCongr'_apply

Mathlib.Logic.Equiv.Basic

URI: https://scilib.ai/kg/mathlib#Equiv.piCongr'_apply

English

The application of piCongr' to a dependent function f is the function b ↦ h2(b)(f(h1⁻¹(b))).

Русский

Применение piCongr' к зависимой функции f даёт b ↦ h2(b)(f(h1⁻¹(b))).

LaTeX

$$$\\forall f:\\,(\\forall a, W a),\\quad \\text{piCongr'}\\,f = (b\\mapsto h_2(b)\\big( f(h_1^{-1}(b))\\big)).$$$

Lean4

theorem piCongr'_apply (f : ∀ a, W a) : h₁.piCongr' h₂ f = fun b => h₂ b <| f <| h₁.symm b :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru