left_notMem

Mathlib.Analysis.Convex.Side

URI: https://scilib.ai/kg/mathlib#AffineSubspace.SSameSide.left_notMem

English

If h is SS ameSide, then both left and right not mem hold.

Русский

Если h является SS ameSide, левая и правая не принадлежат s.

LaTeX

$$$$ h.2.1 \text{ and } h.2.2 \rightarrow \neg (x \in s) \land \neg (y \in s). $$$$

Lean4

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

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru