wOppSide — Mathlib

English

Let s be an affine subspace of P and x, y points of P. If x and y lie on opposite sides of s (in the strong sense), then they also lie on opposite sides of s in the weaker sense.

Русский

Пусть s — аффинное подпространство P и x, y ∈ P. Если x и y лежат по разные стороны s в сильном смысле, то они также лежат по разные стороны s в слабом смысле.

LaTeX

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

Lean4

theorem wOppSide {s : AffineSubspace R P} {x y : P} (h : s.SOppSide x y) : s.WOppSide x y :=
  h.1

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