How to indicate two points are on different sides of a line

Stream: Is there code for X?

[yulia wang]

I want to prove some theorems about parallel and commit it to mathlib. But I don't know how to indicate that two points are on different sides of a straight line

theorem alternate_angles_eq_parallel {E F A C : P} (ℓ₁ ℓ₂ t : AffineSubspace k P)
  (hE : E ∈ ℓ₁ ⊓ t) (hF : F ∈ ℓ₂ ⊓ t) (hEA : E ≠ A) (hFC : F ≠ C)(hA₁ : A ∈ ℓ₁) (hC₂ : C ∈ ℓ₂)
  (hAng : ∠ A E F = ∠ C F E) : ℓ₁ ∥ ℓ₂ := by
  by_contra
  sorry

[yulia wang]

Just like alternate_angles_eq_parallel. How to describe C and A on both sides of t?

[Aaron Liu]

maybe use an oriented angle?

[Aaron Liu]

in more than two dimensions lines don't really have "sides"

[yulia wang]

Thank you very much . I will use oriented angle to finish it.

[Joseph Myers]

We have AffineSubspace.SOppSide as the predicate for two points being on opposite sides of an affine subspace.