OAI/Analysis/ProductSpaces/ClosedTails.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.IndependentProducts.path_generator_set_eq line 14
  2. lemma OAI.IndependentProducts.dense_pathVector_span line 25
  3. def OAI.IndependentProducts.FiniteHead.headSpan line 46
  4. instance OAI.IndependentProducts.FiniteHead.headSpan_finiteDimensional line 49
  5. def OAI.IndependentProducts.FiniteHead.relativeVector line 53

    Source documentation

    Relative tail products, algebraically equal to sums of outside-head jumps.

    def relativeVector (v : Vertex) : productSpan μ :=
…

    Mentions: OAI.IndependentProducts.Vertex, OAI.IndependentProducts.productSpan

  6. def OAI.IndependentProducts.FiniteHead.tailAlgebraic line 56
  7. def OAI.IndependentProducts.FiniteHead.tailSpace line 59
  8. lemma OAI.IndependentProducts.FiniteHead.relativeVector_mem line 61
  9. lemma OAI.IndependentProducts.FiniteHead.headSpan_sup_tailSpace line 66
  10. lemma OAI.IndependentProducts.FiniteHead.tailSpace_cofinite line 89