wOppSide_self_iff — Mathlib

English

Equivalence: s.WOppSide x x ↔ x ∈ s.

Русский

Для любого подпространства s и точки x ∈ P, s.WOppSide x x эквивалентно x ∈ s.

LaTeX

$$$s.WOppSide x x \iff x \in s.$$$

Lean4

@[simp]
theorem wOppSide_self_iff {s : AffineSubspace R P} {x : P} : s.WOppSide x x ↔ x ∈ s :=
  by
  constructor
  · rintro ⟨p₁, hp₁, p₂, hp₂, h⟩
    obtain ⟨a, -, -, -, -, h₁, -⟩ := h.exists_eq_smul_add
    rw [add_comm, vsub_add_vsub_cancel, ← eq_vadd_iff_vsub_eq] at h₁
    rw [h₁]
    exact s.smul_vsub_vadd_mem a hp₂ hp₁ hp₁
  · exact fun h => ⟨x, h, x, h, SameRay.rfl⟩

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