mem_of_wbtw — Mathlib

English

Let s be an affine subspace of P. If x, y, z ∈ P satisfy Wbtw R x y z and x, z ∈ s, then y ∈ s.

Русский

Пусть s — аффинное подпространство P. Если x, y, z ∈ P удовлетворяют Wbtw R x y z и x, z ∈ s, то y ∈ s.

LaTeX

$$Wbtw R x y z \land x \in s \land z \in s \Rightarrow y \in s$$

Lean4

theorem mem_of_wbtw {s : AffineSubspace R P} {x y z : P} (hxyz : Wbtw R x y z) (hx : x ∈ s) (hz : z ∈ s) : y ∈ s := by
  obtain ⟨ε, -, rfl⟩ := hxyz; exact lineMap_mem _ hx hz

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