Scaling transfers any proof of the side-three lower bound.

The scaling corollary

def ConwaySoifer.EquilateralTriangle.scale (T : EquilateralTriangle) (c : ℝ) (hc : 0 ≤ c) : EquilateralTriangle

The triangle scaled by c > 0 about the origin.

Equations

• T.scale c hc = { vertices := fun (i : Fin 3) => c • T.vertices i, side := c * T.side, side_nonneg := ⋯, equilateral := ⋯ }

theorem ConwaySoifer.EquilateralTriangle.carrier_scale (T : EquilateralTriangle) (c : ℝ) (hc : 0 ≤ c) : (T.scale c hc).carrier = c • T.carrier

theorem ConwaySoifer.no_ten_unit_triangle_cover_of_lowerBound (hLB : LowerBound) (ε : ℝ) (hε : 0 < ε) (T : Configuration) (hs : ∀ (i : Fin 10), (T i).side = 1) (hcover : ∀ p ∈ (1 + ε / 3) • target, ∃ (i : Fin 10), p ∈ (T i).carrier) : False

Ten unit triangles cannot cover the triangle of side 3 + ε: the target scaled by (3 + ε)/3 = 1 + ε/3.