The supported move at a free triangle

This file transports the normalized thin-kite move to an arbitrary plane triangle. Compactness supplies the small positive thickness required by the relative polygonal Schoenflies theorem.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.affineEquivHomeomorph (e : Plane ≃ᵃ[ℝ] Plane) : Plane ≃ₜ Plane

An affine equivalence of the plane, regarded as a homeomorphism.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.Moise.affineEquivHomeomorph e = { toEquiv := e.toEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.affineEquivHomeomorph_apply (e : Plane ≃ᵃ[ℝ] Plane) (p : Plane) : (affineEquivHomeomorph e) p = e p

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.affineEquivHomeomorph_symm_apply (e : Plane ≃ᵃ[ℝ] Plane) (p : Plane) : (affineEquivHomeomorph e).symm p = e.symm p

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.affineEquivHomeomorph_image_segment (e : Plane ≃ᵃ[ℝ] Plane) (a b : Plane) : ⇑(affineEquivHomeomorph e) '' segment ℝ a b = segment ℝ (e a) (e b)

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.transportedThinKiteHomeomorph (e : Plane ≃ᵃ[ℝ] Plane) (δ : ℝ) (hδ : 0 < δ) : Plane ≃ₜ Plane

Conjugate the normalized kite move by an affine coordinate system.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.Moise.transportedThinKitePatch (e : Plane ≃ᵃ[ℝ] Plane) (δ : ℝ) : Set Plane

The transportedThinKitePatch declaration.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.Moise.transportedThinKitePatch e δ = ⇑e '' LeanEval.Topology.ClassificationOfSurfaces.Moise.thinKitePatch δ

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.transportedThinKiteHomeomorph_eqOn_compl (e : Plane ≃ᵃ[ℝ] Plane) (δ : ℝ) (hδ : 0 < δ) : Set.EqOn (⇑(transportedThinKiteHomeomorph e δ hδ)) id (transportedThinKitePatch e δ)ᶜ

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.transportedThinKiteHomeomorph_image_baseSegment (e : Plane ≃ᵃ[ℝ] Plane) (δ : ℝ) (hδ : 0 < δ) : ⇑(transportedThinKiteHomeomorph e δ hδ) '' segment ℝ (e (planePoint (-1) 0)) (e (planePoint 1 0)) = segment ℝ (e (planePoint (-1) 0)) (e (planePoint 0 1)) ∪ segment ℝ (e (planePoint 1 0)) (e (planePoint 0 1))

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.exists_thinKitePatch_subset_open (e : Plane ≃ᵃ[ℝ] Plane) (U : Set Plane) (hU : IsOpen U) (htriangle : ⇑e '' (convexHull ℝ) (Set.range kiteTrianglePosition) ⊆ U) : ∃ (δ : ℝ), 0 < δ ∧ transportedThinKitePatch e δ ⊆ U

A sufficiently thin transported kite lies in every open neighborhood of its limiting triangle.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.exists_eventually_transportedThinKitePatch_subset_open (e : Plane ≃ᵃ[ℝ] Plane) (U : Set Plane) (hU : IsOpen U) (htriangle : ⇑e '' (convexHull ℝ) (Set.range kiteTrianglePosition) ⊆ U) : ∃ (ε : ℝ), 0 < ε ∧ ∀ (δ : ℝ), 0 < δ → δ < ε → transportedThinKitePatch e δ ⊆ U

Uniform version of exists_thinKitePatch_subset_open: every smaller positive thickness also lies in the prescribed open set.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.freeTriangleOrder (M : TriangleMesh) (T : M.Triangle) (k : Fin 3) : Fin 3 → Plane

Order a triangle so that index 2 is a specified opposite vertex.

Equations

• M.freeTriangleOrder T k i = M.position (M.orderedVertex T ((Equiv.swap 2 k) i))

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.freeTriangleOrder_affineIndependent (M : TriangleMesh) (T : M.Triangle) (k : Fin 3) : AffineIndependent ℝ (M.freeTriangleOrder T k)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.range_freeTriangleOrder (M : TriangleMesh) (T : M.Triangle) (k : Fin 3) : Set.range (M.freeTriangleOrder T k) = M.position '' ↑↑T

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.triangle_eq_orderedVertices (M : TriangleMesh) (T : M.Triangle) : ↑T = {M.orderedVertex T 0, M.orderedVertex T 1, M.orderedVertex T 2}

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.triangleEdges_eq_orderedEdges (M : TriangleMesh) (T : M.Triangle) : M.triangleEdges ↑T = {{M.orderedVertex T 0, M.orderedVertex T 1}, {M.orderedVertex T 0, M.orderedVertex T 2}, {M.orderedVertex T 1, M.orderedVertex T 2}}

def LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.IsOneEdgeFreeTriangle (M : TriangleMesh) (T : M.Triangle) (k : Fin 3) : Prop

Moise's first free-triangle case: the frontier meets the triangle in exactly its base edge.

Equations

• M.IsOneEdgeFreeTriangle T k = (frontier M.toPlaneComplex.support ∩ M.triangleCarrier ↑T = segment ℝ (M.freeTriangleOrder T k 0) (M.freeTriangleOrder T k 1))

def LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.IsTwoEdgeFreeTriangle (M : TriangleMesh) (T : M.Triangle) (k : Fin 3) : Prop

Moise's second free-triangle case: the frontier meets the triangle in exactly the two edges through the apex.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.IsGeometricallyFreeTriangle (M : TriangleMesh) (T : M.Triangle) : Prop

The IsGeometricallyFreeTriangle declaration.

Equations

• M.IsGeometricallyFreeTriangle T = ∃ (k : Fin 3), M.IsOneEdgeFreeTriangle T k ∨ M.IsTwoEdgeFreeTriangle T k

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.freeTriangleBase_diff_endpoints_disjoint_apexEdges (M : TriangleMesh) (T : M.Triangle) (k : Fin 3) : Disjoint (segment ℝ (M.freeTriangleOrder T k 0) (M.freeTriangleOrder T k 1) \ {M.freeTriangleOrder T k 0, M.freeTriangleOrder T k 1}) (segment ℝ (M.freeTriangleOrder T k 0) (M.freeTriangleOrder T k 2) ∪ segment ℝ (M.freeTriangleOrder T k 1) (M.freeTriangleOrder T k 2))

The relative interior of the base in the Figure 3.3 ordering misses both apex edges.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.freeTriangleBaseEdge (M : TriangleMesh) (T : M.Triangle) (k : Fin 3) : Finset M.Vertex

The abstract mesh edge underlying the base in the Figure 3.3 ordering.

Equations

• M.freeTriangleBaseEdge T k = Finset.image (M.orderedVertex T) (Finset.univ.erase k)

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.freeTriangleApexEdge0 (M : TriangleMesh) (T : M.Triangle) (k : Fin 3) : Finset M.Vertex

The first abstract edge from a base endpoint to the apex.

Equations

• M.freeTriangleApexEdge0 T k = {M.orderedVertex T ((Equiv.swap 2 k) 0), M.orderedVertex T ((Equiv.swap 2 k) 2)}

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.freeTriangleApexEdge1 (M : TriangleMesh) (T : M.Triangle) (k : Fin 3) : Finset M.Vertex

The second abstract edge from a base endpoint to the apex.

Equations

• M.freeTriangleApexEdge1 T k = {M.orderedVertex T ((Equiv.swap 2 k) 1), M.orderedVertex T ((Equiv.swap 2 k) 2)}

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.freeTriangleBaseEdge_card (M : TriangleMesh) (T : M.Triangle) (k : Fin 3) : (M.freeTriangleBaseEdge T k).card = 2

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.freeTriangleBaseEdge_subset (M : TriangleMesh) (T : M.Triangle) (k : Fin 3) : M.freeTriangleBaseEdge T k ⊆ ↑T

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.freeTriangleBaseEdge_mem_edges (M : TriangleMesh) (T : M.Triangle) (k : Fin 3) : M.freeTriangleBaseEdge T k ∈ M.edges

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.freeTriangleApexEdge0_card (M : TriangleMesh) (T : M.Triangle) (k : Fin 3) : (M.freeTriangleApexEdge0 T k).card = 2

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.freeTriangleApexEdge1_card (M : TriangleMesh) (T : M.Triangle) (k : Fin 3) : (M.freeTriangleApexEdge1 T k).card = 2

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.freeTriangleApexEdge0_subset (M : TriangleMesh) (T : M.Triangle) (k : Fin 3) : M.freeTriangleApexEdge0 T k ⊆ ↑T

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.freeTriangleApexEdge1_subset (M : TriangleMesh) (T : M.Triangle) (k : Fin 3) : M.freeTriangleApexEdge1 T k ⊆ ↑T

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.freeTriangleApexEdge0_mem_edges (M : TriangleMesh) (T : M.Triangle) (k : Fin 3) : M.freeTriangleApexEdge0 T k ∈ M.edges

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.freeTriangleApexEdge1_mem_edges (M : TriangleMesh) (T : M.Triangle) (k : Fin 3) : M.freeTriangleApexEdge1 T k ∈ M.edges

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.image_freeTriangleBaseEdge (M : TriangleMesh) (T : M.Triangle) (k : Fin 3) : M.position '' ↑(M.freeTriangleBaseEdge T k) = {M.freeTriangleOrder T k 0, M.freeTriangleOrder T k 1}

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.freeTriangleBaseEdge_eq_orderedPair (M : TriangleMesh) (T : M.Triangle) (k : Fin 3) : M.freeTriangleBaseEdge T k = {M.orderedVertex T ((Equiv.swap 2 k) 0), M.orderedVertex T ((Equiv.swap 2 k) 1)}

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.freeTriangleBaseEdge_carrier (M : TriangleMesh) (T : M.Triangle) (k : Fin 3) : (convexHull ℝ) (M.position '' ↑(M.freeTriangleBaseEdge T k)) = segment ℝ (M.freeTriangleOrder T k 0) (M.freeTriangleOrder T k 1)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.freeTriangleApexEdge0_carrier (M : TriangleMesh) (T : M.Triangle) (k : Fin 3) : (convexHull ℝ) (M.position '' ↑(M.freeTriangleApexEdge0 T k)) = segment ℝ (M.freeTriangleOrder T k 0) (M.freeTriangleOrder T k 2)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.freeTriangleApexEdge1_carrier (M : TriangleMesh) (T : M.Triangle) (k : Fin 3) : (convexHull ℝ) (M.position '' ↑(M.freeTriangleApexEdge1 T k)) = segment ℝ (M.freeTriangleOrder T k 1) (M.freeTriangleOrder T k 2)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.triangleEdges_eq_freeTriangleEdges (M : TriangleMesh) (T : M.Triangle) (k : Fin 3) : M.triangleEdges ↑T = {M.freeTriangleBaseEdge T k, M.freeTriangleApexEdge0 T k, M.freeTriangleApexEdge1 T k}

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.triangleVertex_mem_freeTriangleApexEdges (M : TriangleMesh) (T : M.Triangle) (k : Fin 3) {v : M.Vertex} (hv : v ∈ ↑T) : M.position v ∈ segment ℝ (M.freeTriangleOrder T k 0) (M.freeTriangleOrder T k 2) ∪ segment ℝ (M.freeTriangleOrder T k 1) (M.freeTriangleOrder T k 2)

Every triangle vertex lies on one of the two apex edges.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.frontier_triangleCarrier_subset_freeTriangleEdges (M : TriangleMesh) (T : M.Triangle) (k : Fin 3) : frontier (M.triangleCarrier ↑T) ⊆ segment ℝ (M.freeTriangleOrder T k 0) (M.freeTriangleOrder T k 1) ∪ (segment ℝ (M.freeTriangleOrder T k 0) (M.freeTriangleOrder T k 2) ∪ segment ℝ (M.freeTriangleOrder T k 1) (M.freeTriangleOrder T k 2))

The frontier of a maximal triangle is covered by the base and the two apex edges in every Figure 3.3 ordering.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.freeTriangleBaseSegment_eq_oppositeEdgeCarrier (M : TriangleMesh) (T : M.Triangle) (k : Fin 3) : segment ℝ (M.freeTriangleOrder T k 0) (M.freeTriangleOrder T k 1) = (convexHull ℝ) ↑(M.oppositeEdgePoints T k)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.isGeometricallyFreeTriangle_of_boundaryEdges_card_one (M : TriangleMesh) (T : M.Triangle) (hvertices : M.HasNoIsolatedFrontierVertex ↑T) (hcard : (M.boundaryEdges ↑T).card = 1) : M.IsGeometricallyFreeTriangle T

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.isGeometricallyFreeTriangle_of_boundaryEdges_card_two (M : TriangleMesh) (T : M.Triangle) (hvertices : M.HasNoIsolatedFrontierVertex ↑T) (hcard : (M.boundaryEdges ↑T).card = 2) : M.IsGeometricallyFreeTriangle T

Moise's second free-triangle case: if exactly two edges of a triangle lie on the mesh frontier, their common endpoint can be chosen as the apex of the Figure 3.3 move.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.isGeometricallyFreeTriangle_of_isFreeTriangle (M : TriangleMesh) (T U : M.Triangle) (hfree : M.IsFreeTriangle ↑T) (hne : ↑T ≠ ↑U) (hneighbors : M.AreEdgeNeighbors ↑T ↑U) (hvertices : M.HasNoIsolatedFrontierVertex ↑T) : M.IsGeometricallyFreeTriangle T

The finite conclusion used by Moise's cutting induction. Once a weakly free triangle has an edge-neighbor and no isolated frontier vertex, its frontier trace is one of the two configurations in Figure 3.3.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.exists_cutting_diagonal_configuration (M : TriangleMesh) (T U : M.Triangle) (hfree : M.IsFreeTriangle ↑T) (hne : ↑T ≠ ↑U) (hneighbors : M.AreEdgeNeighbors ↑T ↑U) (hnot : ¬M.HasNoIsolatedFrontierVertex ↑T) : ∃ (a : M.Vertex) (b : M.Vertex) (v : M.Vertex), a ≠ b ∧ v ≠ a ∧ v ≠ b ∧ ↑T = {a, b, v} ∧ M.boundaryEdges ↑T = {{a, b}} ∧ M.position v ∈ frontier M.toPlaneComplex.support

The exact diagonal configuration in the hard branch of Moise Chapter 3, Theorem 3. If a weakly free triangle is not one of the Figure 3.3 configurations, it has one boundary edge and an isolated opposite boundary vertex; the other two edges are the cutting diagonals.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.freeTriangleAffineEquiv (M : TriangleMesh) (T : M.Triangle) (k : Fin 3) : Plane ≃ᵃ[ℝ] Plane

Affine coordinates taking the normalized kite triangle to T.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.freeTriangleAffineEquiv_apply_vertex (M : TriangleMesh) (T : M.Triangle) (k i : Fin 3) : (M.freeTriangleAffineEquiv T k) (kiteTrianglePosition i) = M.freeTriangleOrder T k i

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.freeTriangleAffineEquiv_image_triangle (M : TriangleMesh) (T : M.Triangle) (k : Fin 3) : ⇑(M.freeTriangleAffineEquiv T k) '' (convexHull ℝ) (Set.range kiteTrianglePosition) = M.triangleCarrier ↑T

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.exists_transportedThinKitePatch_inter_boundaryEdge_subset_baseEndpoints (M : TriangleMesh) (T : M.Triangle) (k : Fin 3) (htrace : frontier M.toPlaneComplex.support ∩ M.triangleCarrier ↑T = segment ℝ (M.freeTriangleOrder T k 0) (M.freeTriangleOrder T k 1)) (e : Finset M.Vertex) (he : M.IsBoundaryEdge e) (hne : e ≠ M.freeTriangleBaseEdge T k) : ∃ (ε : ℝ), 0 < ε ∧ ∀ (δ : ℝ), 0 < δ → δ < ε → transportedThinKitePatch (M.freeTriangleAffineEquiv T k) δ ∩ (convexHull ℝ) (M.position '' ↑e) ⊆ {M.freeTriangleOrder T k 0, M.freeTriangleOrder T k 1}

Every boundary edge other than the base of a one-edge move is avoided by all sufficiently thin transported kites, except possibly at the two base endpoints.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.exists_supported_triangle_push_fixing_boundaryCarrier (M : TriangleMesh) (T : M.Triangle) (k : Fin 3) (htrace : frontier M.toPlaneComplex.support ∩ M.triangleCarrier ↑T = segment ℝ (M.freeTriangleOrder T k 0) (M.freeTriangleOrder T k 1)) (U : Set Plane) (hU : IsOpen U) (hTU : M.triangleCarrier ↑T ⊆ U) : ∃ (δ : ℝ) (hδ : 0 < δ), Set.EqOn (⇑(transportedThinKiteHomeomorph (M.freeTriangleAffineEquiv T k) δ hδ)) id Uᶜ ∧ Set.EqOn (⇑(transportedThinKiteHomeomorph (M.freeTriangleAffineEquiv T k) δ hδ)) id (M.boundaryCarrier \ M.triangleCarrier ↑T) ∧ ⇑(transportedThinKiteHomeomorph (M.freeTriangleAffineEquiv T k) δ hδ) '' segment ℝ (M.freeTriangleOrder T k 0) (M.freeTriangleOrder T k 1) = segment ℝ (M.freeTriangleOrder T k 0) (M.freeTriangleOrder T k 2) ∪ segment ℝ (M.freeTriangleOrder T k 1) (M.freeTriangleOrder T k 2)

The one-edge Figure 3.3 push can be made relative both to a prescribed open set and to the entire old boundary carrier away from the deleted triangle.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.exists_supported_triangle_push (M : TriangleMesh) (T : M.Triangle) (k : Fin 3) (U : Set Plane) (hU : IsOpen U) (hTU : M.triangleCarrier ↑T ⊆ U) : ∃ (h : Plane ≃ₜ Plane), Set.EqOn (⇑h) id Uᶜ ∧ ⇑h '' segment ℝ (M.freeTriangleOrder T k 0) (M.freeTriangleOrder T k 1) = segment ℝ (M.freeTriangleOrder T k 0) (M.freeTriangleOrder T k 2) ∪ segment ℝ (M.freeTriangleOrder T k 1) (M.freeTriangleOrder T k 2)

Moise's Figure 3.3 move in an arbitrary free triangle coordinate system, with support in a prescribed open neighborhood of that triangle.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.exists_supported_triangle_pull (M : TriangleMesh) (T : M.Triangle) (k : Fin 3) (U : Set Plane) (hU : IsOpen U) (hTU : M.triangleCarrier ↑T ⊆ U) : ∃ (h : Plane ≃ₜ Plane), Set.EqOn (⇑h) id Uᶜ ∧ ⇑h '' (segment ℝ (M.freeTriangleOrder T k 0) (M.freeTriangleOrder T k 2) ∪ segment ℝ (M.freeTriangleOrder T k 1) (M.freeTriangleOrder T k 2)) = segment ℝ (M.freeTriangleOrder T k 0) (M.freeTriangleOrder T k 1)

The inverse Figure 3.3 move removes a triangle whose two apex edges lie on the frontier.