parallel_comm — Mathlib

English

The symmetric version of parallel: if h is a proof that s1 ∥ s2, then it gives a proof that s2 ∥ s1.

Русский

Симметрическая версия параллельности: если существует свидетельство того, что s1 ∥ s2, то существует свидетельство того, что s2 ∥ s1.

LaTeX

$$h : s_1 \\parallel s_2 ⟹ s_2 \\parallel s_1$$

Lean4

theorem parallel_comm {s₁ s₂ : AffineSubspace k P} : s₁ ∥ s₂ ↔ s₂ ∥ s₁ :=
  ⟨Parallel.symm, Parallel.symm⟩

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