not_wOppSide_bot — Mathlib

English

No pair of points lies on the weak same-side relation when the subspace is the bottom element: for all x,y, not (⊥).WSameSide x y.

Русский

Для нижнего предела подпространств не существует пары точек, удовлетворяющих слабому условию одной стороны: для всех x,y не выполняется ⊥.WSameSide x y.

LaTeX

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

Lean4

theorem not_wOppSide_bot (x y : P) : ¬(⊥ : AffineSubspace R P).WOppSide x y := fun ⟨_, h, _⟩ => h.elim

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