ofEq_rfl

Mathlib.Analysis.Normed.Affine.Isometry

URI: https://scilib.ai/kg/mathlib#AffineIsometryEquiv.ofEq_rfl

English

The coercion of ofEq between subspaces acts trivially on elements, mapping to themselves.

Русский

Приведение к подпространству через ofEq действует тривиально на элементы, отправляя их в самих себя.

LaTeX

$$$\mathrm{toFun}(\mathrm{ofEq}(S_1,S_2,h))(x) = x$ (up to the underlying type's representation)$$

Lean4

@[simp]
theorem ofEq_rfl : ofEq s₁ s₁ rfl = refl 𝕜 s₁ :=
  rfl

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

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

Разделы

Аффилиация

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