The deleted AddCircle is equidecomposable to the AddCircle

This file shows an application of equidecomposition, to the elementary example of a circle being equidecomposable with a circle with a missing point.

Instead of using the Circle structure, we use AddCircle to simplify our proof.

inductive AddCircleRotation : Type

The two potential actions that we can make in our additive circle equidecomposition: stay or move.

• stay : AddCircleRotation
• move : AddCircleRotation

instance instDecidableEqAddCircleRotation : DecidableEq AddCircleRotation

Equations

• instDecidableEqAddCircleRotation x✝ y✝ = if h : x✝.toCtorIdx = y✝.toCtorIdx then isTrue ⋯ else isFalse ⋯

instance instReprAddCircleRotation : Repr AddCircleRotation

Equations

• instReprAddCircleRotation = { reprPrec := reprAddCircleRotation✝ }

instance instTopFinsetAddCircleRotation : Top (Finset AddCircleRotation)

Equations

• instTopFinsetAddCircleRotation = { top := {AddCircleRotation.stay, AddCircleRotation.move} }

@[simp]

theorem AddCircle_coe_zero (r : ℝ) : ↑0 = 0

TODO(mathlib4): PR

noncomputable instance instSMulAddCircleRotationAddCircleReal (r : ℝ) : SMul AddCircleRotation (AddCircle r)

Equations

• instSMulAddCircleRotationAddCircleReal r = { smul := fun (x : AddCircleRotation) (θ : AddCircle r) => if x = AddCircleRotation.move then θ + ↑(-1) else θ }

noncomputable def add_circle_equidecomp (r : ℝ) (hr : Irrational r) (m : AddCircle r) : Equidecomp (AddCircle r) AddCircleRotation

We say that the deleted circle (a circle with one point missing) is equidecomposable with the circle by moving every point that is ℕ+ radians forward from in the deleted circle back by one radian.

Equations

• One or more equations did not get rendered due to their size.