direction_le — Mathlib

English

If one affine subspace is contained in another, then the corresponding directions satisfy inclusion.

Русский

Если одно аффинное подпроизвольное содержится в другом, то их соответствующие направления также входят друг в друга.

LaTeX

$$$\text{If } s_1 \le s_2 \text{, then } \mathrm{dir}(s_1) \le \mathrm{dir}(s_2).$$$

Lean4

/-- If one affine subspace is less than or equal to another, the same applies to their
directions. -/
theorem direction_le {s₁ s₂ : AffineSubspace k P} (h : s₁ ≤ s₂) : s₁.direction ≤ s₂.direction :=
  by
  simp only [direction_eq_vectorSpan, vectorSpan_def]
  exact vectorSpan_mono k h

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