mapsTo_inversion_affineSubspace_of_mem

English

If the center c lies in an affine subspace p, then the inversion with center c and radius R maps p into itself (preserves p).

Русский

Если центр инверсии c принадлежит аффинному подпространству p, то инверсия с центром c и радиусом R отображает p в себя (сохраняет p).

LaTeX

$$$ \text{If } c \in p, \quad \operatorname{MapsTo}(\mathrm{inversion}(c,R), p, p).$$$

Lean4

/-- Inversion sends an affine subspace passing through the center to itself. -/
theorem mapsTo_inversion_affineSubspace_of_mem {p : AffineSubspace ℝ P} (hp : c ∈ p) : MapsTo (inversion c R) p p :=
  fun _ ↦ AffineMap.lineMap_mem _ hp

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