sOppSide_pointReflection — Mathlib

English

If x ∈ s and y ∉ s, then the point reflection of y about x lies on the opposite side of s from y.

Русский

Если x ∈ s и y ∉ s, то отражение y через x лежит на противоположной стороне от y по отношению к s.

LaTeX

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

Lean4

theorem sOppSide_pointReflection {s : AffineSubspace R P} {x y : P} (hx : x ∈ s) (hy : y ∉ s) :
    s.SOppSide y (pointReflection R x y) :=
  by
  refine (sbtw_pointReflection_of_ne R fun h => hy ?_).sOppSide_of_notMem_of_mem hy hx
  rwa [← h]

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