OAI/Analysis/FreeWords/TupleHull.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.KKFactorSupport.TupleSpace line 28
  2. def OAI.KKFactorSupport.tupleVector line 30
  3. def OAI.KKFactorSupport.tupleConj line 33
  4. def OAI.KKFactorSupport.tupleOrbit line 38
  5. def OAI.KKFactorSupport.tupleHull line 41
  6. theorem OAI.KKFactorSupport.tupleConj_apply line 45
  7. theorem OAI.KKFactorSupport.tupleConj_vector line 50
  8. theorem OAI.KKFactorSupport.tupleConj_norm line 55
  9. theorem OAI.KKFactorSupport.mapsTo_hull_codomain line 60
  10. theorem OAI.KKFactorSupport.tupleHull_component line 71
  11. theorem OAI.KKFactorSupport.tupleConj_hull line 82
  12. theorem OAI.KKFactorSupport.tuple_trace_in_hull line 96