OAI/Combinatorics/ContingencyTables/Transport/FiniteGraphRoots.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Explicit least roots of finite graph components

The selector uses the finite reachability closure, not a choice of a quotient representative. Its defining closure runs exactly n growth rounds on Fin n, including disconnected and singleton components.

  1. lemma OAI.ContingencyTables.FiniteGraphRoots.closure_nonempty line 18
  2. def OAI.ContingencyTables.FiniteGraphRoots.root line 22

    Source documentation

    The least actual vertex index in the reached component.

    def root (v : Fin n) : Fin n := (closure G v).min' (closure_nonempty G v)

    Mentions: OAI.ContingencyTables.FiniteGraphRoots.closure_nonempty

  3. lemma OAI.ContingencyTables.FiniteGraphRoots.root_mem line 24
  4. lemma OAI.ContingencyTables.FiniteGraphRoots.root_reachable line 27
  5. lemma OAI.ContingencyTables.FiniteGraphRoots.closure_eq line 30
  6. lemma OAI.ContingencyTables.FiniteGraphRoots.root_constant line 39
  7. lemma OAI.ContingencyTables.FiniteGraphRoots.root_idempotent line 46
  8. lemma OAI.ContingencyTables.FiniteGraphRoots.root_le line 49
  9. lemma OAI.ContingencyTables.FiniteGraphRoots.root_eq_self_of_minimal line 52