OAI/Analysis/WeakInfiniteness/WordTensorDensity.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.WeakPureInfiniteness.universal_word_span_dense line 25
  2. def OAI.WeakPureInfiniteness.minimalElementaryRightLinear line 55
  3. def OAI.WeakPureInfiniteness.minimalElementaryLeftLinear line 60
  4. def OAI.WeakPureInfiniteness.minimalElementaryRightContinuous line 65
  5. def OAI.WeakPureInfiniteness.minimalElementaryLeftContinuous line 68
  6. lemma OAI.WeakPureInfiniteness.minimal_elementary_span_dense line 73
  7. def OAI.WeakPureInfiniteness.wordTensorLinear line 99
  8. lemma OAI.WeakPureInfiniteness.wordTensorLinear_apply line 102
  9. lemma OAI.WeakPureInfiniteness.wordTensorLinear_range_dense line 105