OAI/Probability/CriticalPercolation/LinearGroups/LocalProjectiveAction.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CriticalPercolation.LocalProjective.nzImage line 15
  2. def OAI.CriticalPercolation.LocalProjective.action line 18
  3. lemma OAI.CriticalPercolation.LocalProjective.action_point line 27
  4. lemma OAI.CriticalPercolation.LocalProjective.action_one line 30
  5. lemma OAI.CriticalPercolation.LocalProjective.action_mul line 34
  6. lemma OAI.CriticalPercolation.LocalProjective.continuous_action line 39
  7. def OAI.CriticalPercolation.LocalProjective.mulAction line 45
  8. lemma OAI.CriticalPercolation.LocalProjective.continuousConstSMul line 50
  9. instance OAI.CriticalPercolation.LocalProjective.spaceMeasurable line 55
  10. instance OAI.CriticalPercolation.LocalProjective.spaceBorel line 56
  11. lemma OAI.CriticalPercolation.LocalProjective.exists_invariant_measure line 58
  12. def OAI.CriticalPercolation.LocalProjective.subspace line 71
  13. lemma OAI.CriticalPercolation.LocalProjective.point_mem_subspace line 74
  14. lemma OAI.CriticalPercolation.LocalProjective.preimage_point_subspace line 83
  15. lemma OAI.CriticalPercolation.LocalProjective.closed_subspace line 88
  16. lemma OAI.CriticalPercolation.LocalProjective.measurable_subspace line 94
  17. lemma OAI.CriticalPercolation.LocalProjective.subspace_inf line 97
  18. lemma OAI.CriticalPercolation.LocalProjective.subspace_bot line 103
  19. lemma OAI.CriticalPercolation.LocalProjective.subspace_top line 109
  20. lemma OAI.CriticalPercolation.LocalProjective.preimage_action_subspace line 114