The elementary supported move in polygonal Schoenflies

This is the normalized version of Moise Figure 3.3. Four triangles fan from a point (0,a) inside a fixed diamond. Repositioning the fan point while fixing the four diamond vertices gives a PL homeomorphism of the diamond, and hence an ambient homeomorphism by identity extension.

def LeanEval.Topology.ClassificationOfSurfaces.Moise.diamondFanPosition (a : ℝ) : Fin 5 → Plane

Vertices 0,1,2,3 are left, right, top, bottom; vertex 4 is the fan point.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.Moise.diamondFanTriangles : Finset (Finset (Fin 5))

The four maximal triangles in the fan of the diamond.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.Moise.diamondFanTriangles = {{0, 4, 2}, {1, 2, 4}, {0, 3, 4}, {1, 4, 3}}

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.diamondFanPosition_apply_zero (a : ℝ) : diamondFanPosition a 0 = planePoint (-1) 0

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.diamondFanPosition_apply_one (a : ℝ) : diamondFanPosition a 1 = planePoint 1 0

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.diamondFanPosition_apply_two (a : ℝ) : diamondFanPosition a 2 = planePoint 0 2

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.diamondFanPosition_apply_three (a : ℝ) : diamondFanPosition a 3 = planePoint 0 (-2)

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.diamondFanPosition_apply_four (a : ℝ) : diamondFanPosition a 4 = planePoint 0 a

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.diamondFanPosition_injective {a : ℝ} (ha0 : -2 < a) (ha1 : a < 2) : Function.Injective (diamondFanPosition a)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.diamondFan_affineIndependent {a : ℝ} (ha0 : -2 < a) (ha2 : a < 2) {t : Finset (Fin 5)} (ht : t ∈ diamondFanTriangles) : AffineIndependent ℝ fun (v : ↥t) => diamondFanPosition a ↑v

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.diamondVerticalAffine : Plane →ᵃ[ℝ] ℝ

Vertical separator for the upper and lower pairs of left/right fan triangles.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.Moise.diamondVerticalAffine = LeanEval.Topology.ClassificationOfSurfaces.Moise.cartesianX

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.diamondLeftAffine (a : ℝ) : Plane →ᵃ[ℝ] ℝ

Separator through the left vertex and fan point.

Equations

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

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.diamondRightAffine (a : ℝ) : Plane →ᵃ[ℝ] ℝ

Separator through the right vertex and fan point.

Equations

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

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.diamondDownDiagonalAffine (a : ℝ) : Plane →ᵃ[ℝ] ℝ

Separator of the upper-left and lower-right opposite fan triangles.

Equations

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

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.diamondUpDiagonalAffine (a : ℝ) : Plane →ᵃ[ℝ] ℝ

Separator of the upper-right and lower-left opposite fan triangles.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.diamondVerticalAffine_apply (x y : ℝ) : diamondVerticalAffine (planePoint x y) = x

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.diamondLeftAffine_apply (a x y : ℝ) : (diamondLeftAffine a) (planePoint x y) = a * x - y + a

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.diamondRightAffine_apply (a x y : ℝ) : (diamondRightAffine a) (planePoint x y) = a * x + y - a

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.diamondDownDiagonalAffine_apply (a x y : ℝ) : (diamondDownDiagonalAffine a) (planePoint x y) = x - y + a

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.diamondUpDiagonalAffine_apply (a x y : ℝ) : (diamondUpDiagonalAffine a) (planePoint x y) = x + y - a

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.triangle_edge_split_union (p : Fin 3 → Plane) (hp : AffineIndependent ℝ p) (c : ℝ) (hc0 : 0 < c) (hc1 : c < 1) : (convexHull ℝ) (Set.range ![p 0, p 2, (AffineMap.lineMap (p 0) (p 1)) c]) ∪ (convexHull ℝ) (Set.range ![p 1, p 2, (AffineMap.lineMap (p 0) (p 1)) c]) = (convexHull ℝ) (Set.range p)

Splitting one edge of a nondegenerate triangle at an interior parameter covers the original triangle by the two resulting triangles.

def LeanEval.Topology.ClassificationOfSurfaces.Moise.diamondLeftRegion : Set Plane

The left triangular half of the fixed diamond.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.Moise.diamondRightRegion : Set Plane

The right triangular half of the fixed diamond.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.Moise.diamondPatch : Set Plane

The fixed closed patch supporting the elementary move.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.isClosed_diamondPatch : IsClosed diamondPatch

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.diamondFan_left_union {a : ℝ} (ha0 : -2 < a) (ha1 : a < 2) : (convexHull ℝ) (diamondFanPosition a '' ↑{0, 4, 2}) ∪ (convexHull ℝ) (diamondFanPosition a '' ↑{0, 3, 4}) = diamondLeftRegion

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.diamondFan_right_union {a : ℝ} (ha0 : -2 < a) (ha1 : a < 2) : (convexHull ℝ) (diamondFanPosition a '' ↑{1, 2, 4}) ∪ (convexHull ℝ) (diamondFanPosition a '' ↑{1, 4, 3}) = diamondRightRegion

@[reducible, inline]

noncomputable abbrev LeanEval.Topology.ClassificationOfSurfaces.Moise.diamondFanMesh (a : ℝ) (ha0 : -2 < a) (ha1 : a < 2) : TriangleMesh

The four-triangle fan of a fixed diamond, with fan point (0,a).

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.diamondFanMesh_support (a : ℝ) (ha0 : -2 < a) (ha1 : a < 2) : (diamondFanMesh a ha0 ha1).toPlaneComplex.support = diamondPatch

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.diamondSlackUR : Plane →ᵃ[ℝ] ℝ

Slack from the upper-right side of the diamond.

Equations

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

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.diamondSlackUL : Plane →ᵃ[ℝ] ℝ

Slack from the upper-left side of the diamond.

Equations

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

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.diamondSlackLR : Plane →ᵃ[ℝ] ℝ

Slack from the lower-right side of the diamond.

Equations

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

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.diamondSlackLL : Plane →ᵃ[ℝ] ℝ

Slack from the lower-left side of the diamond.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.diamondSlackUR_apply (x y : ℝ) : diamondSlackUR (planePoint x y) = 2 - 2 * x - y

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.diamondSlackUL_apply (x y : ℝ) : diamondSlackUL (planePoint x y) = 2 + 2 * x - y

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.diamondSlackLR_apply (x y : ℝ) : diamondSlackLR (planePoint x y) = 2 - 2 * x + y

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.diamondSlackLL_apply (x y : ℝ) : diamondSlackLL (planePoint x y) = 2 + 2 * x + y

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.diamondSlackUR_eq (p : Plane) : diamondSlackUR p = 2 - 2 * p.ofLp 0 - p.ofLp 1

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.diamondSlackUL_eq (p : Plane) : diamondSlackUL p = 2 + 2 * p.ofLp 0 - p.ofLp 1

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.diamondSlackLR_eq (p : Plane) : diamondSlackLR p = 2 - 2 * p.ofLp 0 + p.ofLp 1

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.diamondSlackLL_eq (p : Plane) : diamondSlackLL p = 2 + 2 * p.ofLp 0 + p.ofLp 1

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.diamondSlackUR_baryEval (a : ℝ) (ha0 : -2 < a) (ha1 : a < 2) (x : Fin 5 → ℝ) (hsum : ∑ v : Fin 5, x v = 1) : diamondSlackUR ((diamondFanMesh a ha0 ha1).toPlaneComplex.baryEval x) = 4 * x 0 + 4 * x 3 + (2 - a) * x 4

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.diamondSlackUL_baryEval (a : ℝ) (ha0 : -2 < a) (ha1 : a < 2) (x : Fin 5 → ℝ) (hsum : ∑ v : Fin 5, x v = 1) : diamondSlackUL ((diamondFanMesh a ha0 ha1).toPlaneComplex.baryEval x) = 4 * x 1 + 4 * x 3 + (2 - a) * x 4

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.diamondSlackLR_baryEval (a : ℝ) (ha0 : -2 < a) (ha1 : a < 2) (x : Fin 5 → ℝ) (hsum : ∑ v : Fin 5, x v = 1) : diamondSlackLR ((diamondFanMesh a ha0 ha1).toPlaneComplex.baryEval x) = 4 * x 0 + 4 * x 2 + (2 + a) * x 4

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.diamondSlackLL_baryEval (a : ℝ) (ha0 : -2 < a) (ha1 : a < 2) (x : Fin 5 → ℝ) (hsum : ∑ v : Fin 5, x v = 1) : diamondSlackLL ((diamondFanMesh a ha0 ha1).toPlaneComplex.baryEval x) = 4 * x 1 + 4 * x 2 + (2 + a) * x 4

def LeanEval.Topology.ClassificationOfSurfaces.Moise.InDiamond (p : Plane) : Prop

Closed four-halfspace description of the diamond.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.diamondPatch_eq_inDiamond : diamondPatch = {p : Plane | InDiamond p}

def LeanEval.Topology.ClassificationOfSurfaces.Moise.StrictlyInDiamond : Set Plane

Points satisfying all four diamond inequalities strictly form an open subset of the patch.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.baryEval_mem_strictlyInDiamond_of_center_pos (a : ℝ) (ha0 : -2 < a) (ha1 : a < 2) (x : Fin 5 → ℝ) (h0 : ∀ (v : Fin 5), 0 ≤ x v) (hsum : ∑ v : Fin 5, x v = 1) (h4 : 0 < x 4) : (diamondFanMesh a ha0 ha1).toPlaneComplex.baryEval x ∈ StrictlyInDiamond

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.isOpen_strictlyInDiamond : IsOpen StrictlyInDiamond

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.strictlyInDiamond_subset_patch : StrictlyInDiamond ⊆ diamondPatch

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.strictlyInDiamond_subset_interior : StrictlyInDiamond ⊆ interior diamondPatch

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.diamondFanReposition (a b : ℝ) (ha0 : -2 < a) (ha1 : a < 2) (hb0 : -2 < b) (hb1 : b < 2) : TriangleMesh

The fixed abstract diamond fan with its center repositioned from height a to height b.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.diamondFanReposition_support (a b : ℝ) (ha0 : -2 < a) (ha1 : a < 2) (hb0 : -2 < b) (hb1 : b < 2) : (diamondFanReposition a b ha0 ha1 hb0 hb1).toPlaneComplex.support = diamondPatch

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.diamondFanReposition_support_eq_source (a b : ℝ) (ha0 : -2 < a) (ha1 : a < 2) (hb0 : -2 < b) (hb1 : b < 2) : (diamondFanReposition a b ha0 ha1 hb0 hb1).toPlaneComplex.support = (diamondFanMesh a ha0 ha1).toPlaneComplex.support

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.diamondFanReposition_baryEval_eq_of_center_zero (a b : ℝ) (ha0 : -2 < a) (ha1 : a < 2) (hb0 : -2 < b) (hb1 : b < 2) (x : Fin 5 → ℝ) (h4 : x 4 = 0) : (diamondFanReposition a b ha0 ha1 hb0 hb1).toPlaneComplex.baryEval x = (diamondFanMesh a ha0 ha1).toPlaneComplex.baryEval x

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.diamondFanSupportHomeomorph (a b : ℝ) (ha0 : -2 < a) (ha1 : a < 2) (hb0 : -2 < b) (hb1 : b < 2) : ↑(diamondFanMesh a ha0 ha1).toPlaneComplex.support ≃ₜ ↑(diamondFanReposition a b ha0 ha1 hb0 hb1).toPlaneComplex.support

Preserve barycentric coordinates while moving the fan point from (0,a) to (0,b).

Equations

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

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.diamondFanCenterRealization (a : ℝ) (ha0 : -2 < a) (ha1 : a < 2) : ↑(GeometricRealization (Fin 5) (diamondFanMesh a ha0 ha1).toPlaneComplex.cells)

The diamondFanCenterRealization declaration.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.Moise.diamondFanCenterRealization a ha0 ha1 = ⟨Pi.single 4 1, ⋯⟩

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.diamondFanCenterRealization_baryEval (a : ℝ) (ha0 : -2 < a) (ha1 : a < 2) : (diamondFanMesh a ha0 ha1).toPlaneComplex.baryEval ↑(diamondFanCenterRealization a ha0 ha1) = planePoint 0 a

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.diamondFanSupportHomeomorph_center (a b : ℝ) (ha0 : -2 < a) (ha1 : a < 2) (hb0 : -2 < b) (hb1 : b < 2) : ↑((diamondFanSupportHomeomorph a b ha0 ha1 hb0 hb1) ⟨planePoint 0 a, ⋯⟩) = planePoint 0 b

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.diamondFanPatchHomeomorph (a b : ℝ) (ha0 : -2 < a) (ha1 : a < 2) (hb0 : -2 < b) (hb1 : b < 2) : ↑(diamondFanMesh a ha0 ha1).toPlaneComplex.support ≃ₜ ↑(diamondFanMesh a ha0 ha1).toPlaneComplex.support

The barycentric fan move, viewed as a self-homeomorphism of the original diamond support.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.diamondFanPatchHomeomorph_apply_val (a b : ℝ) (ha0 : -2 < a) (ha1 : a < 2) (hb0 : -2 < b) (hb1 : b < 2) (z : ↑(diamondFanMesh a ha0 ha1).toPlaneComplex.support) : ↑((diamondFanPatchHomeomorph a b ha0 ha1 hb0 hb1) z) = ↑((diamondFanSupportHomeomorph a b ha0 ha1 hb0 hb1) z)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.diamondFanPatchHomeomorph_fixed_frontier (a b : ℝ) (ha0 : -2 < a) (ha1 : a < 2) (hb0 : -2 < b) (hb1 : b < 2) (p : Plane) (hp : p ∈ frontier (diamondFanMesh a ha0 ha1).toPlaneComplex.support) : ↑((diamondFanPatchHomeomorph a b ha0 ha1 hb0 hb1) ⟨p, ⋯⟩) = p

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.diamondFanAmbientHomeomorph (a b : ℝ) (ha0 : -2 < a) (ha1 : a < 2) (hb0 : -2 < b) (hb1 : b < 2) : Plane ≃ₜ Plane

The elementary fan move extended by the identity to the whole plane.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.diamondFanAmbientHomeomorph_center (a b : ℝ) (ha0 : -2 < a) (ha1 : a < 2) (hb0 : -2 < b) (hb1 : b < 2) : (diamondFanAmbientHomeomorph a b ha0 ha1 hb0 hb1) (planePoint 0 a) = planePoint 0 b

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.diamondFanAmbientHomeomorph_eqOn_compl (a b : ℝ) (ha0 : -2 < a) (ha1 : a < 2) (hb0 : -2 < b) (hb1 : b < 2) : Set.EqOn (⇑(diamondFanAmbientHomeomorph a b ha0 ha1 hb0 hb1)) id diamondPatchᶜ