not_sOppSide — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem not_sOppSide {s : AffineSubspace R P} {x y : P} (h : s.WSameSide x y) : ¬s.SOppSide x y :=
  by
  intro ho
  have hxy := wSameSide_and_wOppSide_iff.1 ⟨h, ho.1⟩
  rcases hxy with (hx | hy)
  · exact ho.2.1 hx
  · exact ho.2.2 hy

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