congr_fun

Mathlib.Analysis.Normed.Operator.LinearIsometry

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

English

The ext lemma states that two LinearIsometryEquiv are equal if they agree pointwise.

Русский

Лемма ext утверждает, что две LinearIsometryEquiv равны, если они совпадают на каждой точке.

LaTeX

$$$\\forall x, e(x)=e'(x) \\Rightarrow e=e'$$$

Lean4

protected theorem congr_fun {f g : E ≃ₛₗᵢ[σ₁₂] E₂} (h : f = g) (x : E) : f x = g x :=
  h ▸ rfl

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

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

Разделы

Аффилиация

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