OAI/Combinatorics/HadwigerCounterexample/TensorIntersections.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Tensor Intersections

  1. theorem OAI.HadwigerCounterexample.colSp_join line 18
  2. theorem OAI.HadwigerCounterexample.colSp_primary line 34
  3. theorem OAI.HadwigerCounterexample.join_kernel line 39
  4. theorem OAI.HadwigerCounterexample.colSp_lift_le line 52
  5. theorem OAI.HadwigerCounterexample.rank_lift_le line 58
  6. theorem OAI.HadwigerCounterexample.rank_lift_eq line 62
  7. def OAI.HadwigerCounterexample.joins line 78

    Source documentation

    Sum of dimensions of the kernel of the combined plus maps at each component. This bounds (in fact equals) the sum of intersection dimensions of full plus frames when the frames are valid.

    def joins (x : UnitType p n N) : ℕ :=
…

    Mentions: OAI.HadwigerCounterexample.UnitType

  8. theorem OAI.HadwigerCounterexample.totalRank_shared line 81
  9. theorem OAI.HadwigerCounterexample.eta_share line 102
  10. def OAI.HadwigerCounterexample.parityW line 114
  11. theorem OAI.HadwigerCounterexample.parityW_shared line 116