not_sOppSide_self

Mathlib.Analysis.Convex.Side

URI: https://scilib.ai/kg/mathlib#AffineSubspace.not_sOppSide_self

English

For any affine subspace s and any x, s.SOppSide x x is impossible.

Русский

Для любого an affine subspace s и любой точки x, s.SOppSide x x невозможно.

LaTeX

$$$\neg s.SOppSide x x$$$

Lean4

theorem not_sOppSide_self (s : AffineSubspace R P) (x : P) : ¬s.SOppSide x x :=
  by
  rw [SOppSide]
  simp

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

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

Разделы

Аффилиация

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