OAI/Topology/CoarseAssembly/SampledHomotopyDecomposition.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Endpoint and interior decompositions of finite homotopy samples

  1. def OAI.CoarseAssembly.Analytic.sampledFiniteSum_head_tail line 15
  2. def OAI.CoarseAssembly.Analytic.lastEndpointFirst line 40

    Source documentation

    Put the last endpoint first, leaving the interior list in its original order.

    def lastEndpointFirst (N : ℕ) (τ : ℕ → Interval) (j : ℕ) : Interval :=
…

    Mentions: OAI.CoarseAssembly.Analytic.Interval

  3. theorem OAI.CoarseAssembly.Analytic.lastEndpointFirst_zero line 43
  4. theorem OAI.CoarseAssembly.Analytic.lastEndpointFirst_succ line 46
  5. def OAI.CoarseAssembly.Analytic.sampledFiniteSum_rotate line 49