wSameSide₁₂

Mathlib.Analysis.Convex.Side

URI: https://scilib.ai/kg/mathlib#Wbtw.wSameSide₁₂

English

If h encodes a Wbtw triple and z ∈ s, then s.WSameSide x y.

Русский

Если h кодирует тройку Wbtw и z ∈ s, то s.WSameSide x y.

LaTeX

$$$\forall s:\text{AffineSubspace } R P\ ,\forall x,y,z\in P\ , (h:Wbtw\ R x y z)\ , hz:\ z \in s\Rightarrow s.WSameSide x y.$$$

Lean4

theorem _root_.Wbtw.wSameSide₁₂ {s : AffineSubspace R P} {x y z : P} (h : Wbtw R x y z) (hz : z ∈ s) :
    s.WSameSide x y :=
  h.symm.wSameSide₃₂ hz

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

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

Разделы

Аффилиация

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