V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
⊢ sin (∠ p₁ p₂ p₃) = 0 → Collinear ℝ {p₁, p₂, p₃}
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : sin (∠ p₁ p₂ p₃) = 0
⊢ Collinear ℝ {p₁, p₂, p₃}
revert h
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
⊢ ¬Collinear ℝ {p₁, p₂, p₃} → ¬sin (∠ p₁ p₂ p₃) = 0
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
⊢ sin (∠ p₁ p₂ p₃) = 0 → Collinear ℝ {p₁, p₂, p₃}
contrapose
no goals
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
⊢ ¬Collinear ℝ {p₁, p₂, p₃} → ¬sin (∠ p₁ p₂ p₃) = 0
exact sin_ne_zero_of_not_collinear