symm — Mathlib

English

If s1 ∥ s2, then s2 ∥ s1. The parallel relation is symmetric.

Русский

Если s1 параллельно s2, то и s2 параллельно s1. Отношение параллельности симметрично.

LaTeX

$$s_1 \\parallel s_2 \\;\\Rightarrow\\; s_2 \\parallel s_1$$

Lean4

@[symm]
theorem symm {s₁ s₂ : AffineSubspace k P} (h : s₁ ∥ s₂) : s₂ ∥ s₁ :=
  by
  rcases h with ⟨v, rfl⟩
  refine ⟨-v, ?_⟩
  rw [map_map, ← coe_trans_to_affineMap, ← constVAdd_add, neg_add_cancel, constVAdd_zero, coe_refl_to_affineMap, map_id]

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