not_sOppSide_bot — Mathlib

English

Similarly, no pair of points lies on the strong same-side relation when the bottom subspace is used: for all x,y, not (⊥).SSameSide x y.

Русский

Аналогично: для нижнего подпространства не выполняется SSameSide.

LaTeX

$$$\forall x,y:\; \neg (\bot : AffineSubspace(R,P)).SSameSide\; x\; y$$$

Lean4

theorem not_sOppSide_bot (x y : P) : ¬(⊥ : AffineSubspace R P).SOppSide x y := fun h => not_wOppSide_bot x y h.wOppSide

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