k : Type u_2
V : Type u_3
P : Type u_1
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type ?u.337806
s : Set P
⊢ affineSpan k s ≠ ⊥ ↔ s ≠ ∅
k : Type u_2
V : Type u_3
P : Type u_1
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type ?u.337806
s : Set P
⊢ ⊥ < affineSpan k s ↔ Set.Nonempty s
rw [bot_lt_iff_ne_bot, nonempty_iff_ne_empty]
no goals
k : Type u_2
V : Type u_3
P : Type u_1
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type ?u.337806
s : Set P
⊢ affineSpan k s ≠ ⊥ ↔ s ≠ ∅
exact (affineSpan_eq_bot _).not