image_eq_preimage — Mathlib

English

For a linear isometry equivalence e, and any subset s, the image of s under e equals the preimage of s under e’s inverse: e[s] = (e^{-1})[s].

Русский

Для линейного исометрического эквивалента e для любого множества s выполняется e[s] = (e^{-1})[s].

LaTeX

$$$e[S] = e^{-1}[S]$ for all S$$

Lean4

theorem image_eq_preimage (s : Set E) : e '' s = e.symm ⁻¹' s :=
  e.toLinearEquiv.image_eq_preimage s

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