OAI/Topology/ArtinGroups/Harmonic/Extend.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.HarmonicArtin.NullBoundary.continuousLinearMap_eq_zero_of_interior_max line 11
  2. def OAI.HarmonicArtin.NullBoundary.extend line 22
  3. lemma OAI.HarmonicArtin.NullBoundary.extend_apply_mem line 26
  4. lemma OAI.HarmonicArtin.NullBoundary.extend_apply_not_mem line 31
  5. lemma OAI.HarmonicArtin.NullBoundary.extend_restrict line 36
  6. lemma OAI.HarmonicArtin.NullBoundary.extend_dot line 46
  7. def OAI.HarmonicArtin.NullBoundary.coordFunctional line 57
  8. lemma OAI.HarmonicArtin.NullBoundary.coordFunctional_apply line 60
  9. lemma OAI.HarmonicArtin.NullBoundary.null_mulVec_nonpos line 65
  10. lemma OAI.HarmonicArtin.NullBoundary.null_pairing_nonpos line 78
  11. lemma OAI.HarmonicArtin.NullBoundary.null_pairing_eq_zero_boundary line 88
  12. lemma OAI.HarmonicArtin.NullBoundary.convexHull_bound line 112
  13. theorem OAI.HarmonicArtin.NullBoundary.convex_null_boundary_separation line 133