right_notMem — Mathlib

English

Let s be an affine subspace of P and x,y points of P. If s.SOppSide x y holds, then the right point y is not contained in s.

Русский

Пусть s — аффинное подпространство P и x,y ∈ P. При выполнении s.SOppSide x y левый элемент x не принадлежит s, а правая точка y не принадлежит s.

LaTeX

$$$\forall s: \text{AffineSubspace}(R,P)\ \forall x,y: P,\; s.SOppSide\; x\; y \Rightarrow y \notin s$$$

Lean4

theorem right_notMem {s : AffineSubspace R P} {x y : P} (h : s.SOppSide x y) : y ∉ s :=
  h.2.2

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