reflection_mem_subspace_eq_self

Mathlib.Analysis.InnerProductSpace.Projection.Reflection

URI: https://scilib.ai/kg/mathlib#Submodule.reflection_mem_subspace_eq_self

English

If x belongs to K, then x is fixed by reflection in K.

Русский

Если x принадлежит K, то отражение в K оставляет x без изменений.

LaTeX

$$$x \in K \implies R_K(x) = x$$$

Lean4

theorem reflection_mem_subspace_eq_self {x : E} (hx : x ∈ K) : K.reflection x = x :=
  (reflection_eq_self_iff x).mpr hx

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

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

Разделы

Аффилиация

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