A side-parameter-compatible polygon cell model for a triangle

This file identifies the three-sided PolygonCell with the standard closed triangle. The boundary calibration is exact: circular side i at parameter t is sent to the affine point at parameter t on standard triangle edge i.

theorem LeanEval.Topology.ClassificationOfSurfaces.TriangleCell.instFactLtRealOfNat_leanPool : Fact (0 < 3)

@[reducible, inline]

abbrev LeanEval.Topology.ClassificationOfSurfaces.TriangleCell.StandardTriangle : Set Moise.Plane

The closed standard triangle, viewed as a topological subspace.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.TriangleCell.StandardTriangle = LeanEval.Topology.ClassificationOfSurfaces.Moise.standardTrianglePlaneComplex.support

@[reducible, inline]

abbrev LeanEval.Topology.ClassificationOfSurfaces.TriangleCell.StandardTriangleBoundary : Set Moise.Plane

The frontier of the standard triangle.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.TriangleCell.StandardTriangleBoundary = frontier LeanEval.Topology.ClassificationOfSurfaces.Moise.standardTrianglePlaneComplex.support

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.TriangleCell.boundaryParam (x : ℝ) : Moise.Plane

Traverse the three affine sides of the standard triangle during the interval [0, 3].

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.TriangleCell.continuous_boundaryParam : Continuous boundaryParam

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.TriangleCell.boundaryParam_zero : boundaryParam 0 = Moise.standardTriangleVertex 0

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.TriangleCell.boundaryParam_one : boundaryParam 1 = Moise.standardTriangleVertex 1

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.TriangleCell.boundaryParam_two : boundaryParam 2 = Moise.standardTriangleVertex 2

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.TriangleCell.boundaryParam_three : boundaryParam 3 = Moise.standardTriangleVertex 0

theorem LeanEval.Topology.ClassificationOfSurfaces.TriangleCell.boundaryParam_mem_frontier {x : ℝ} (hx : x ∈ Set.Icc 0 3) : boundaryParam x ∈ StandardTriangleBoundary

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.TriangleCell.boundaryParamIcc (x : ↑(Set.Icc 0 (0 + 3))) : ↑StandardTriangleBoundary

The affine boundary traversal, with its frontier-membership proof.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.TriangleCell.boundaryParamIcc x = ⟨LeanEval.Topology.ClassificationOfSurfaces.TriangleCell.boundaryParam ↑x, ⋯⟩

theorem LeanEval.Topology.ClassificationOfSurfaces.TriangleCell.continuous_boundaryParamIcc : Continuous boundaryParamIcc

theorem LeanEval.Topology.ClassificationOfSurfaces.TriangleCell.boundaryParamIcc_zero_eq_three : boundaryParamIcc ⟨0, ⋯⟩ = boundaryParamIcc ⟨3, ⋯⟩

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.TriangleCell.boundaryQuotMap : Quot (AddCircle.EndpointIdent 3 0) → ↑StandardTriangleBoundary

The quotient of [0,3] with its endpoints identified maps around the standard frontier.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.TriangleCell.continuous_boundaryQuotMap : Continuous boundaryQuotMap

theorem LeanEval.Topology.ClassificationOfSurfaces.TriangleCell.injective_boundaryQuotMap : Function.Injective boundaryQuotMap

theorem LeanEval.Topology.ClassificationOfSurfaces.TriangleCell.surjective_boundaryQuotMap : Function.Surjective boundaryQuotMap

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.TriangleCell.addCircleBoundaryHomeomorph : AddCircle 3 ≃ₜ ↑StandardTriangleBoundary

The additive circle of circumference three is the standard triangular frontier.

Equations

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

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.TriangleCell.circleBoundaryHomeomorph : Circle ≃ₜ ↑StandardTriangleBoundary

The complex unit circle is the standard triangular frontier.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.TriangleCell.circleBoundaryHomeomorph_side (i : Fin 3) (t : ↑unitInterval) : circleBoundaryHomeomorph (Circle.exp (PolygonCell.sideAngle i t)) = ⟨(AffineMap.lineMap (Moise.standardTriangleVertex i) (Moise.standardTriangleVertex ((finRotate 3) i))) ↑t, ⋯⟩

theorem LeanEval.Topology.ClassificationOfSurfaces.TriangleCell.exists_triangleAmbientHomeomorph : ∃ (h : Moise.Plane ≃ₜ ℂ), ⇑h '' Moise.standardTrianglePlaneComplex.support = Metric.closedBall 0 1 ∧ ⇑h '' frontier Moise.standardTrianglePlaneComplex.support = Metric.sphere 0 1

An ambient straightening of the standard triangle to the Euclidean closed unit disk.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.TriangleCell.triangleAmbientHomeomorph : Moise.Plane ≃ₜ ℂ

The triangleAmbientHomeomorph declaration.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.TriangleCell.triangleAmbientHomeomorph = Classical.choose LeanEval.Topology.ClassificationOfSurfaces.TriangleCell.exists_triangleAmbientHomeomorph

theorem LeanEval.Topology.ClassificationOfSurfaces.TriangleCell.triangleAmbientHomeomorph_image_triangle : ⇑triangleAmbientHomeomorph '' Moise.standardTrianglePlaneComplex.support = Metric.closedBall 0 1

theorem LeanEval.Topology.ClassificationOfSurfaces.TriangleCell.triangleAmbientHomeomorph_image_boundary : ⇑triangleAmbientHomeomorph '' frontier Moise.standardTrianglePlaneComplex.support = Metric.sphere 0 1

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.TriangleCell.triangleDiskHomeomorph : ↑StandardTriangle ≃ₜ PolygonCell 3

Restrict the ambient straightening to the closed triangle.

Equations

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

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.TriangleCell.boundaryCircleHomeomorph : ↑StandardTriangleBoundary ≃ₜ Circle

The ambient straightening restricted to the standard triangular frontier.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.TriangleCell.boundaryInclusion : C(↑StandardTriangleBoundary, ↑StandardTriangle)

Include the standard frontier in the closed standard triangle.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.TriangleCell.triangleDiskHomeomorph_boundary (z : ↑StandardTriangleBoundary) : triangleDiskHomeomorph (boundaryInclusion z) = (PolygonCell.ofCircle 3) (boundaryCircleHomeomorph z)

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.TriangleCell.cellHomeomorph : PolygonCell 3 ≃ₜ ↑StandardTriangle

The calibrated homeomorphism from the three-sided cell to the standard triangle.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.TriangleCell.cellHomeomorph_ofCircle (z : Circle) : cellHomeomorph ((PolygonCell.ofCircle 3) z) = boundaryInclusion (circleBoundaryHomeomorph z)

theorem LeanEval.Topology.ClassificationOfSurfaces.TriangleCell.cellHomeomorph_side (i : Fin 3) (t : ↑unitInterval) : cellHomeomorph ((PolygonCell.side i) t) = ⟨(AffineMap.lineMap (Moise.standardTriangleVertex i) (Moise.standardTriangleVertex ((finRotate 3) i))) ↑t, ⋯⟩