English
If one nonempty affine subspace s1 is strictly contained in s2, then their directions satisfy a strict inclusion: dir(s1) < dir(s2).
Русский
Если непустое подпространство s1 строго вложено в s2, то их направления удовлетворяют строгому включению: dir(s1) < dir(s2).
LaTeX
$$$ s_1 < s_2 \\\\Rightarrow s_1.direction < s_2.direction \\\\text{(assuming nonempty s1). } $$$
Lean4
/-- If one nonempty affine subspace is less than another, the same applies to their directions -/
theorem direction_lt_of_nonempty {s₁ s₂ : AffineSubspace k P} (h : s₁ < s₂) (hn : (s₁ : Set P).Nonempty) :
s₁.direction < s₂.direction := by
obtain ⟨p, hp⟩ := hn
rw [lt_iff_le_and_exists] at h
rcases h with ⟨hle, p₂, hp₂, hp₂s₁⟩
rw [SetLike.lt_iff_le_and_exists]
use direction_le hle, p₂ -ᵥ p, vsub_mem_direction hp₂ (hle hp)
intro hm
rw [vsub_right_mem_direction_iff_mem hp p₂] at hm
exact hp₂s₁ hm
