Adaptive triangulations subordinate to an open cover

The adaptive fan construction only needs a hereditary, locally attainable notion of a safe midpoint face. This file instantiates that interface with containment in one member of an open cover. In particular, the resulting locally finite triangulation has every closed triangle in one prescribed control neighborhood. Quantitative chart approximation can therefore choose the neighborhoods first and reuse the conforming triangulation unchanged.

structure LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.AdaptiveOpenCover (K : IntrinsicTwoComplex) (U : Set K.realization) : Type 1

An open cover of U by subsets which remain inside U.

• Index : Type

  The Index declaration.

• set : self.Index → Set K.realization

  The set declaration.

• isOpen (i : self.Index) : IsOpen (self.set i)
• subset (i : self.Index) : self.set i ⊆ U
• covers {p : K.realization} : p ∈ U → ∃ (i : self.Index), p ∈ self.set i

@[reducible]

def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.AdaptiveOpenCover.safety (K : IntrinsicTwoComplex) (U : Set K.realization) (C : K.AdaptiveOpenCover U) : K.AdaptiveSafety U

A level face is cover-safe when its complete carrier lies in one cover member.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.AdaptiveOpenCover.safety_isAdmissible (K : IntrinsicTwoComplex) (U : Set K.realization) (C : K.AdaptiveOpenCover U) : AdaptiveSafety.IsAdmissible K U

Subordination to an open cover is locally attainable under repeated midpoint subdivision.

@[reducible, inline]

noncomputable abbrev LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.AdaptiveOpenCover.locallyFiniteTriangleComplex (K : IntrinsicTwoComplex) (U : Set K.realization) (C : K.AdaptiveOpenCover U) (hU : IsOpen U) : LocallyFiniteTriangleComplex ↑U

The conforming adaptive triangle complex subordinate to C.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.AdaptiveOpenCover.locallyFiniteTriangleComplex K U C hU = K.adaptiveLocallyFiniteTriangleComplex U hU

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.AdaptiveOpenCover.locallyFiniteTriangleComplex_support (K : IntrinsicTwoComplex) (U : Set K.realization) (C : K.AdaptiveOpenCover U) (hU : IsOpen U) : (locallyFiniteTriangleComplex K U C hU).support = Set.univ

The cover-subordinate adaptive complex covers all of U.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.AdaptiveOpenCover.faceVertices_injective (K : IntrinsicTwoComplex) (U : Set K.realization) (C : K.AdaptiveOpenCover U) (hU : IsOpen U) : Function.Injective (locallyFiniteTriangleComplex K U C hU).faceVertices

Distinct faces of the cover-subordinate adaptive complex carry distinct vertex triples.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.AdaptiveOpenCover.exists_cover_set_of_adaptiveFace (K : IntrinsicTwoComplex) (U : Set K.realization) (C : K.AdaptiveOpenCover U) (t : K.AdaptiveFace U) : ∃ (i : C.Index), K.adaptiveFaceCarrier U t ⊆ C.set i

Every adaptive tile selected by C lies in one member of the cover.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.AdaptiveOpenCover.exists_cover_set_of_complex_face (K : IntrinsicTwoComplex) (U : Set K.realization) (C : K.AdaptiveOpenCover U) (hU : IsOpen U) (f : (locallyFiniteTriangleComplex K U C hU).Face) : ∃ (i : C.Index), Subtype.val '' (locallyFiniteTriangleComplex K U C hU).faceCarrier f ⊆ C.set i

Every closed triangle of the conforming fan triangulation lies in one cover member.