OAI/Analysis/FreeWords/PartialWords.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.KKLocalPatching.PatchingWord line 18
  2. def OAI.KKLocalPatching.PatchingWord.tailValue line 28
  3. def OAI.KKLocalPatching.PatchingWord.value line 31
  4. def OAI.KKLocalPatching.PatchingWord.length line 34
  5. theorem OAI.KKLocalPatching.PatchingWord.tailValue_nil line 36
  6. theorem OAI.KKLocalPatching.PatchingWord.tailValue_cons line 38
  7. theorem OAI.KKLocalPatching.PatchingWord.value_zero line 41
  8. theorem OAI.KKLocalPatching.PatchingWord.tailValue_append line 44
  9. theorem OAI.KKLocalPatching.PatchingWord.concrete_norm_one_le line 64
  10. theorem OAI.KKLocalPatching.PatchingWord.norm_tailValue_le line 69
  11. theorem OAI.KKLocalPatching.PatchingWord.tendsto_tailValue line 83
  12. theorem OAI.KKLocalPatching.PatchingWord.tendsto_value line 101