Construction_of_Triangle_from_Given_Lengths
Provedgeometryproofwikitriangles
Given three straight lines such that the sum of the lengths of any two is greater than the third, it is possible to construct a triangle with those lengths.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Construction_of_Triangle_from_Given_Lengths (a b c : ℝ) (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) (h1 : a + b > c) (h2 : b + c > a) (h3 : a + c > b) : ∃ (x y : ℝ × ℝ), dist x y = c := by sorry
Source