OAI/Geometry/Convex/GeneralMahler/Rigid/Support.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

§06 equality from strict signs, support of two layer functionals.

  1. lemma OAI.GeneralMahler.sZeroPt line 11
  2. lemma OAI.GeneralMahler.s0n line 15
  3. lemma OAI.GeneralMahler.m0 line 21
  4. lemma OAI.GeneralMahler.ProjField.pt_czero line 27
  5. lemma OAI.GeneralMahler.ProjField.nu_comm line 48
  6. lemma OAI.GeneralMahler.ProjField.BLzero line 67
  7. lemma OAI.GeneralMahler.ProjField.B_layer line 92