trans — Mathlib

English

If s1 ∥ s2 and s2 ∥ s3, then s1 ∥ s3.

Русский

Если s1 параллельно s2 и s2 параллельно s3, то s1 параллельно s3.

LaTeX

$$s_1 \\parallel s_2 \\rightarrow s_2 \\parallel s_3 \\rightarrow s_1 \\parallel s_3$$

Lean4

@[trans]
theorem trans {s₁ s₂ s₃ : AffineSubspace k P} (h₁₂ : s₁ ∥ s₂) (h₂₃ : s₂ ∥ s₃) : s₁ ∥ s₃ :=
  by
  rcases h₁₂ with ⟨v₁₂, rfl⟩
  rcases h₂₃ with ⟨v₂₃, rfl⟩
  refine ⟨v₂₃ + v₁₂, ?_⟩
  rw [map_map, ← coe_trans_to_affineMap, ← constVAdd_add]

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