directionOfNonempty_eq_direction — Mathlib

English

For any affine subspace s with a nonempty underlying set, its directional subspace is equal to the direction obtained from any witness of nonemptiness; i.e., directionOfNonempty h = s.direction when h asserts nonemptiness.

Русский

Для любой аффинной подпространственной части s с непустым подмножеством точек имеется равенство направления; directionOfNonempty h = s.direction при неравенстве.

LaTeX

$$$\operatorname{directionOfNonempty}(h) = s.direction$$$

Lean4

/-- `direction_of_nonempty` gives the same submodule as `direction`. -/
theorem directionOfNonempty_eq_direction {s : AffineSubspace k P} (h : (s : Set P).Nonempty) :
    directionOfNonempty h = s.direction :=
  by
  refine le_antisymm ?_ (Submodule.span_le.2 Set.Subset.rfl)
  rw [← SetLike.coe_subset_coe, directionOfNonempty, direction, Submodule.coe_set_mk, AddSubmonoid.coe_set_mk]
  exact vsub_set_subset_vectorSpan k _

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