K : Type u_2
V : Type u_1
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
S : Set (ℙ K V)
u : ℙ K V
⊢ u ∈ span S ↔ ∀ (W : Subspace K V), span S ≤ W → u ∈ W
K : Type u_2
V : Type u_1
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
S : Set (ℙ K V)
u : ℙ K V
⊢ u ∈ span S ↔ ∀ (W : Subspace K V), S ⊆ ↑W → u ∈ W
simp_rw [← span_le_subspace_iff]
no goals
K : Type u_2
V : Type u_1
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
S : Set (ℙ K V)
u : ℙ K V
⊢ u ∈ span S ↔ ∀ (W : Subspace K V), span S ≤ W → u ∈ W
exact ⟨fun hu W hW => hW hu, fun W => W (span S) (le_refl _)⟩