image_inversion_affineSubspace_of_mem

English

If a subspace p contains the center c, then the image of p under inversion with center c and radius R is p itself.

Русский

Если подпространство p содержит центр инверсии c, то образ p под инверсией с центром c и радиусом R равен самому p.

LaTeX

$$$ \mathrm{image}(\mathrm{inversion}(c,R), p) = p \quad \text{when } c \in p.$$$

Lean4

/-- Inversion sends an affine subspace passing through the center to itself. -/
theorem image_inversion_affineSubspace_of_mem {p : AffineSubspace ℝ P} (hR : R ≠ 0) (hp : c ∈ p) :
    inversion c R '' p = p :=
  (mapsTo_inversion_affineSubspace_of_mem hp).image_subset.antisymm fun x hx ↦
    ⟨inversion c R x, mapsTo_inversion_affineSubspace_of_mem hp hx, inversion_inversion _ hR _⟩

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