not_wOppSide — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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