affineSpan_eq_top_iff_vectorSpan_eq_top_of_nonempty

English

For nonempty sets, the top equivalence holds similarly even under nontrivial assumptions.

Русский

Для непустых множеств верно аналогично без дополнительных ограничений.

LaTeX

$$affineSpan k s = ⊤ ↔ vectorSpan k s = ⊤, при условии nonempty s$$

Lean4

/-- For a nonempty set, the affine span is `⊤` iff its vector span is `⊤`. -/
theorem affineSpan_eq_top_iff_vectorSpan_eq_top_of_nonempty {s : Set P} (hs : s.Nonempty) :
    affineSpan k s = ⊤ ↔ vectorSpan k s = ⊤ :=
  by
  refine ⟨vectorSpan_eq_top_of_affineSpan_eq_top k V P, ?_⟩
  intro h
  suffices Nonempty (affineSpan k s) by
    obtain ⟨p, hp : p ∈ affineSpan k s⟩ := this
    rw [eq_iff_direction_eq_of_mem hp (mem_top k V p), direction_affineSpan, h, direction_top]
  obtain ⟨x, hx⟩ := hs
  exact ⟨⟨x, mem_affineSpan k hx⟩⟩

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