OAI/Combinatorics/ContingencyTables/Transport/TableMarginTransport.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Changing equal margin descriptions without changing entries

  1. def OAI.ContingencyTables.tableFintypeTransport line 11

    Source documentation

    Enumeration instances affect the proofs of the margins, never the entries.

    def tableFintypeTransport (fi fi' : Fintype I) (fj fj' : Fintype J)
    (r : I → ℕ) (c : J → ℕ) : @Table I J fi fj r c ≃ @Table I J fi' fj' r c where
…

    Mentions: OAI.ContingencyTables.Table

  2. def OAI.ContingencyTables.tableMarginTransport line 24