OAI/Combinatorics/HadwigerCounterexample/TerminalCut.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Terminal Cut

  1. def OAI.HadwigerCounterexample.pairCaps line 14

    Source documentation

    Individual marginal caps (mapW denotes the actual marginals) and a joint cap.

    def pairCaps (μ : Wgt α) (m d : ℝ) (w : Wgt (α × α)) :=
…

    Mentions: OAI.HadwigerCounterexample.Wgt

  2. theorem OAI.HadwigerCounterexample.closed_pairCaps line 19
  3. theorem OAI.HadwigerCounterexample.mid_pairCaps line 31
  4. theorem OAI.HadwigerCounterexample.compact_subLaw line 46
  5. def OAI.HadwigerCounterexample.incW line 61
  6. theorem OAI.HadwigerCounterexample.incW_tot line 64
  7. theorem OAI.HadwigerCounterexample.incW_pr line 68
  8. theorem OAI.HadwigerCounterexample.sat_le_tot line 77
  9. theorem OAI.HadwigerCounterexample.mapW_tot' line 88
  10. theorem OAI.HadwigerCounterexample.terminal line 91