left_notMem — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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