not_wSameSide — Mathlib

English

If two points lie on opposite sides of an affine subspace, then they do not lie on the same weak side.

Русский

Если две точки лежат на противоположных сторонах аффинного подпространства, то они не лежат на одной слабой стороне.

LaTeX

$$$\\\\forall s : \\mathrm{AffineSubspace}\\\\ R P, \\\\forall x y : P, s.WOppSide x y \\\\Rightarrow ¬ s.WSameSide x y$$$

Lean4

theorem not_wSameSide {s : AffineSubspace R P} {x y : P} (h : s.SOppSide x y) : ¬s.WSameSide x y := fun hs =>
  hs.not_sOppSide h

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