wSameSide₂₁

Mathlib.Analysis.Convex.Side

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

English

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

Русский

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

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 y x.$$$

Lean4

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

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

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

Разделы

Аффилиация

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