congr_fun

Mathlib.Topology.Algebra.ContinuousAffineMap

URI: https://scilib.ai/kg/mathlib#ContinuousAffineMap.congr_fun

English

If e1: P1 ≃ᴬ[k] P2 and e2: P3 ≃ᴬ[k] P4, then congruent points in the product map accordingly.

Русский

Если e1: P1 ≃ᴬ[k] P2 и e2: P3 ≃ᴬ[k] P4, то отображение на произведении согласуется по координатам.

LaTeX

$$$\forall p=(p_1,p_3),\quad (e_1.prodCongr e_2)(p) = (e_1(p_1), e_2(p_3)).$$$

Lean4

theorem congr_fun {f g : P →ᴬ[R] Q} (h : f = g) (x : P) : f x = g x :=
  DFunLike.congr_fun h _

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

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

Разделы

Аффилиация

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