wSameSide_self_iff — Mathlib

English

A point lies on the weak same-side relation with itself exactly when the corresponding affine subspace is nonempty.

Русский

Точка лежит в отношении слабой одной стороны с самой собой тогда и только тогда, когда соответствующее аффинное подпространоство непусто.

LaTeX

$$$ s.WSameSide x x \iff (s : Set P).Nonempty $$$

Lean4

@[simp]
theorem wSameSide_self_iff {s : AffineSubspace R P} {x : P} : s.WSameSide x x ↔ (s : Set P).Nonempty :=
  ⟨fun h => h.nonempty, fun ⟨p, hp⟩ => ⟨p, hp, p, hp, SameRay.rfl⟩⟩

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