Positive anchors for the Moise plane structures

Concrete instances required by the definition-faithfulness rules (docs/AUTOFORMALIZATION_GUIDE.md): the standard triangle with vertices (0,0), (1,0), (0,1) realizes

• a PolygonalCircle (standardTriangleCircle): its boundary as a polygonal simple closed curve with three vertices and three edges; and
• a PlaneComplex (standardTrianglePlaneComplex): the full simplicial complex of the closed triangle, with three vertices, three edges and one 2-face (all seven nonempty vertex subsets).

Both geometric side conditions (consecutive_inter, face_inter) reduce to AffineIndependent.convexHull_inter: convex hulls of subfamilies of an affinely independent family intersect in the hull of the shared vertices. The only genuinely geometric input is the affine independence of the three vertices, proved from non-collinearity by coordinate computation.

def LeanEval.Topology.ClassificationOfSurfaces.Moise.standardTriangleVertex : Fin 3 → Plane

The vertices of the standard triangle: (0,0), (1,0), (0,1).

Equations

• LeanEval.Topology.ClassificationOfSurfaces.Moise.standardTriangleVertex = ![!₂[0, 0], !₂[1, 0], !₂[0, 1]]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.standardTriangle_not_collinear : ¬Collinear ℝ {!₂[0, 0], !₂[1, 0], !₂[0, 1]}

The vertices of the standard triangle are not collinear.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.standardTriangleVertex_affineIndependent : AffineIndependent ℝ standardTriangleVertex

The vertices of the standard triangle are affinely independent.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.standardTriangleVertex_injective : Function.Injective standardTriangleVertex

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.standardTriangleVertex_triple_affineIndependent (a b c : Fin 3) (h : Function.Injective ![a, b, c]) : AffineIndependent ℝ ![standardTriangleVertex a, standardTriangleVertex b, standardTriangleVertex c]

Any relabelling of the standard triangle vertices by an injective index vector is affinely independent.

def LeanEval.Topology.ClassificationOfSurfaces.Moise.standardTriangleCircle : PolygonalCircle

Positive anchor for PolygonalCircle: the boundary of the standard triangle with vertices (0,0), (1,0), (0,1) is a polygonal simple closed curve.

Equations

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

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.planeAffineBasisOfTriple (p : Fin 3 → Plane) (hp : AffineIndependent ℝ p) : AffineBasis (Fin 3) ℝ Plane

Three affinely independent points in the plane form an affine basis.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.Moise.planeAffineBasisOfTriple p hp = { toFun := p, ind' := hp, tot' := ⋯ }

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.interior_convexHull_affineBasis (b : AffineBasis (Fin 3) ℝ Plane) : interior ((convexHull ℝ) (Set.range ⇑b)) = {x : Plane | ∀ (i : Fin 3), 0 < (b.coord i) x}

The interior of a full-dimensional plane triangle consists exactly of points with all three barycentric coordinates positive.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.standardTriangleAffineBasis : AffineBasis (Fin 3) ℝ Plane

The standard triangle vertices, regarded as an affine basis of the plane.

Equations

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

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.standardTriangleSimplex : Affine.Simplex ℝ Plane 2

The standard triangle as an affine simplex.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.standardTriangleCircle_carrier : standardTriangleCircle.carrier = frontier ((convexHull ℝ) (Set.range standardTriangleVertex))

The carrier of standardTriangleCircle is the frontier of the closed standard triangle.

@[reducible, inline]

noncomputable abbrev LeanEval.Topology.ClassificationOfSurfaces.Moise.standardTrianglePlaneComplex : PlaneComplex

Positive anchor for PlaneComplex: the closed standard triangle as a simplicial complex, with the seven nonempty subsets of its three vertices as faces.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.standardTrianglePlaneComplex_position : standardTrianglePlaneComplex.position = standardTriangleVertex