wOppSide₃₁ — Mathlib

English

Symmetric version of the previous with the indices swapped.

Русский

Симметричная версия предыдущего утверждения с поменянными индексациями.

LaTeX

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

Lean4

theorem _root_.Wbtw.wOppSide₃₁ {s : AffineSubspace R P} {x y z : P} (h : Wbtw R x y z) (hy : y ∈ s) : s.WOppSide z x :=
  h.symm.wOppSide₁₃ hy

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