coe_ofEq_apply

Mathlib.Analysis.Normed.Operator.LinearIsometry

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

English

If hpq expresses equality p = q and x ∈ p, then the image of x under the equality-based isometry is just x in E.

Русский

Если hpq задаёт равенство p = q и x ∈ p, то образ x под изометрией по равенству равно самому x в E.

LaTeX

$$$hpq : p = q \;\; x \in p \implies (ofEq(p,q,hpq)\,x : E) = x$$$

Lean4

@[simp]
theorem coe_ofEq_apply (h : p = q) (x : p) : (ofEq p q h x : E) = x :=
  rfl

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

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

Разделы

Аффилиация

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