OAI/Geometry/SurfaceImmersion/Atlas/SupportedChartTransport.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Transport smooth compactly supported fields through an actual local coordinate homeomorphism. Extension by zero preserves the original support.

  1. def OAI.ClosedSurfaceR4.JetPolynomial.chartSupport line 21

    Source documentation

    The image compact set for the local coordinate system.

    def chartSupport (e : OpenPartialHomeomorph A B) (K : Compacts A)
    (hK : (K : Set A) ⊆ e.source) : Compacts B :=
…
  2. lemma OAI.ClosedSurfaceR4.JetPolynomial.chartSupport_subset line 26
  3. lemma OAI.ClosedSurfaceR4.JetPolynomial.chartPush_zero line 32
  4. def OAI.ClosedSurfaceR4.JetPolynomial.chartPush line 40
  5. lemma OAI.ClosedSurfaceR4.JetPolynomial.chartPush_apply line 50
  6. def OAI.ClosedSurfaceR4.JetPolynomial.chartPushLM line 55
  7. lemma OAI.ClosedSurfaceR4.JetPolynomial.chartPush_eval_source line 69
  8. lemma OAI.ClosedSurfaceR4.JetPolynomial.chartPush_bound line 76