oangle_ne_zero_and_ne_pi_iff_affineIndependent

English

An oriented angle is neither 0 nor π if and only if the three points are affinely independent.

Русский

Ориентированный угол не равен 0 и не равен π тогда и только тогда, когда три точки аффинно независимы.

LaTeX

$$$ (\angle p_1 p_2 p_3).\mathrm{sign} \neq 0 \land (\angle p_1 p_2 p_3).\mathrm{sign} \neq \pi \;\Longrightarrow\; \text{AffineIndependent } \mathbb{R} \!\![p_1,p_2,p_3] $$$

Lean4

/-- An oriented angle is not zero or `π` if and only if the three points are affinely
independent. -/
theorem oangle_ne_zero_and_ne_pi_iff_affineIndependent {p₁ p₂ p₃ : P} :
    ∡ p₁ p₂ p₃ ≠ 0 ∧ ∡ p₁ p₂ p₃ ≠ π ↔ AffineIndependent ℝ ![p₁, p₂, p₃] :=
  by
  rw [oangle, o.oangle_ne_zero_and_ne_pi_iff_linearIndependent,
    affineIndependent_iff_linearIndependent_vsub ℝ _ (1 : Fin 3), ←
    linearIndependent_equiv (finSuccAboveEquiv (1 : Fin 3))]
  convert Iff.rfl
  ext i
  fin_cases i <;> rfl

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