bot_parallel_iff_eq_bot — Mathlib

English

Two affine subspaces are parallel iff their directions match and either both are bottom or neither is bottom.

Русский

Два аффиновых подпространства параллельны тогда и только тогда, когда их направления совпадают и либо оба являются нулевыми, либо ни одно не является нулевым.

LaTeX

$$$ s_1 \\parallel s_2 \\iff s_1.\\mathrm{direction} = s_2.\\mathrm{direction} \\land (s_1 = \\bot \\iff s_2 = \\bot) $$$

Lean4

@[simp]
theorem bot_parallel_iff_eq_bot {s : AffineSubspace k P} : ⊥ ∥ s ↔ s = ⊥ := by
  rw [parallel_comm, parallel_bot_iff_eq_bot]

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