eq_of_direction_eq_of_nonempty_of_le

English

If two affine subspaces have the same direction, are nonempty, and s1 ⊆ s2, then s1 = s2.

Русский

Если два аффинных подпространства имеют одно и то же направление, непусты и s1 ⊆ s2, то s1 = s2.

LaTeX

$$$\\text{dir}(s_1)=\\text{dir}(s_2) \\land (s_1 \\neq \\varnothing) \\land s_1 \\le s_2 \\Rightarrow s_1 = s_2$$$

Lean4

/-- If an affine subspace is nonempty and contained in another with the same direction, they are
equal. -/
theorem eq_of_direction_eq_of_nonempty_of_le {s₁ s₂ : AffineSubspace k P} (hd : s₁.direction = s₂.direction)
    (hn : (s₁ : Set P).Nonempty) (hle : s₁ ≤ s₂) : s₁ = s₂ :=
  let ⟨p, hp⟩ := hn
  ext_of_direction_eq hd ⟨p, hp, hle hp⟩

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