OAI/Combinatorics/ContingencyTables/Rooted/RootedIntervals.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The actual tree intervals for an explicitly selected component root

The maximum-forest cut estimate applies to every reachable root. Thus the executed least-root convention retains the same finite tree box, including for unbalanced retained small-cell views.

  1. lemma OAI.ContingencyTables.RootedIntervals.nonroot_of_component line 20
  2. theorem OAI.ContingencyTables.RootedIntervals.solved_in_intervals line 27