right_mem_of_wbtw — Mathlib

English

Let s be an affine subspace. If x, y, z are weakly between in Wbtw_R x y z and x, y ∈ s with x ≠ y, then z ∈ s.

Русский

Пусть s – аффинное подпространство. Если x, y, z образуют слабое между, и x, y ∈ s при x ≠ y, тогда z ∈ s.

LaTeX

$$$(Wbtw_R(x,y,z)) \rightarrow (x \in s) \rightarrow (y \in s) \rightarrow (x \neq y) \rightarrow z \in s$$$

Lean4

theorem right_mem_of_wbtw {s : AffineSubspace R P} (hxyz : Wbtw R x y z) (hx : x ∈ s) (hy : y ∈ s) (hxy : x ≠ y) :
    z ∈ s := by
  obtain ⟨ε, -, rfl⟩ := hxyz
  have hε : ε ≠ 0 := by rintro rfl; simp at hxy
  simpa [hε] using lineMap_mem ε⁻¹ hx hy

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