Documentation

LeanPool.NandakumarRamanaRao.HumanVerification.EqualAreaEqualPerimeterPartitionWrapper

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.