sSameSide_self_iff — Mathlib

English

The strong same-side relation of a point with itself is equivalent to the subspace being nonempty and the point not lying in the subspace.

Русский

Строгое отношение SSameSide точки к самой себе эквивалентно тому, что подпространство непусто и точка не принадлежит ему.

LaTeX

$$$ s.SSameSide x x \iff (s : Set P).Nonempty \land x \notin s $$$

Lean4

theorem sSameSide_self_iff {s : AffineSubspace R P} {x : P} : s.SSameSide x x ↔ (s : Set P).Nonempty ∧ x ∉ s :=
  ⟨fun ⟨h, hx, _⟩ => ⟨wSameSide_self_iff.1 h, hx⟩, fun ⟨h, hx⟩ => ⟨wSameSide_self_iff.2 h, hx, hx⟩⟩

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