eq_or_eq_of_orthogonal — Mathlib

English

If four projective points a,b,c,d are pairwise orthogonal in the given pattern, then either a=b or c=d.

Русский

Если четыре точки a,b,c,d удовлетворяют условию ортогональности, то либо a=b, либо c=d.

LaTeX

$$$ a\perp c \wedge b\perp c \wedge a\perp d \wedge b\perp d \Rightarrow (a=b) \lor (c=d)$$$

Lean4

theorem eq_or_eq_of_orthogonal {a b c d : ℙ K (Fin 3 → K)} (hac : a.orthogonal c) (hbc : b.orthogonal c)
    (had : a.orthogonal d) (hbd : b.orthogonal d) : a = b ∨ c = d := by
  induction a with
  | h a ha =>
    induction b with
    | h b hb =>
      induction c with
      | h c hc =>
        induction d with
        | h d hd =>
          rw [mk_eq_mk_iff_crossProduct_eq_zero, mk_eq_mk_iff_crossProduct_eq_zero]
          exact crossProduct_eq_zero_of_dotProduct_eq_zero hac hbc had hbd

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