OAI/Analysis/KadisonKastler/FiniteCornerRefinement.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Compatibility of finite signed corner groups

  1. def OAI.KadisonKastler.cornerSuccessorPermutation line 17

    Source documentation

    Extend a finite permutation by fixing the added last coordinate.

    def cornerSuccessorPermutation (σ : Equiv.Perm (Fin n)) : Equiv.Perm (Fin (n + 1)) :=
…
  2. theorem OAI.KadisonKastler.cornerSuccessorPermutation_castSucc line 21
  3. theorem OAI.KadisonKastler.cornerSuccessorPermutation_last line 26
  4. theorem OAI.KadisonKastler.FullMatrixCorner.finiteSignedDiagonal_succ line 39
  5. theorem OAI.KadisonKastler.FullMatrixCorner.finiteSignedPermutation_succ line 50
  6. theorem OAI.KadisonKastler.FullMatrixCorner.finiteSignedGroup_monotone line 62

    Source documentation

    These concrete finite subgroups increase with the finite corner.

    theorem finiteSignedGroup_monotone : Monotone F.finiteSignedGroup := by
…