wOppSide_pointReflection — Mathlib

English

For any s and any x ∈ s, the point reflection of y about x lies on the opposite side of s from y.

Русский

Для любого s и любого x ∈ s отражение точки y через x лежит на противоположной стороне от y по отношению к s.

LaTeX

$$$\forall s,\forall x\in s:\ s.WOppSide\ y\bigl(\operatorname{pointReflection}(R,x,y)\bigr).$$$

Lean4

theorem wOppSide_pointReflection {s : AffineSubspace R P} {x : P} (y : P) (hx : x ∈ s) :
    s.WOppSide y (pointReflection R x y) :=
  (wbtw_pointReflection R _ _).wOppSide₁₃ hx

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