Equal Area Equal Perimeter Partition Wrapper #
theorem
HumanVerification.equalAreaEqualPerimeterPartitionWrapper
{α : Type}
[NRR.HumanExport.ConvexFigureModel α]
(F : α)
(n : ℕ)
(hn : 0 < n)
:
∃ (pieces : Fin n → α),
NRR.HumanExport.IsConvexPartition F pieces ∧ (∀ (i j : Fin n), NRR.HumanExport.area (pieces i) = NRR.HumanExport.area (pieces j)) ∧ ∀ (i j : Fin n), NRR.HumanExport.perimeter (pieces i) = NRR.HumanExport.perimeter (pieces j)
Internal generic wrapper. Its conclusion is definitionally equal to the
human-facing statement once Main.lean supplies the public
ConvexFigure.instConvexFigureModel instance.