OAI/Combinatorics/HadwigerCounterexample/RankEfficientDecomposition.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Rank Efficient Decomposition

  1. def OAI.HadwigerCounterexample.obsI line 14

    Source documentation

    Evaluation of individual matrices on Xpair

    def obsI (p : Shape) {n} : Individual p n →ₗ[F] ReqF p n where
…

    Mentions: OAI.HadwigerCounterexample.Shape, OAI.HadwigerCounterexample.Individual, OAI.HadwigerCounterexample.F, OAI.HadwigerCounterexample.ReqF

  2. theorem OAI.HadwigerCounterexample.obsI_each line 30
  3. theorem OAI.HadwigerCounterexample.mrk_sub line 34
  4. theorem OAI.HadwigerCounterexample.primary_initial line 37
  5. theorem OAI.HadwigerCounterexample.split_linear line 89