OAI/Analysis/WeakInfiniteness/Hereditary.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.WeakPureInfiniteness.principalRightIdeal line 28
  2. instance OAI.WeakPureInfiniteness.(instance at line 31) line 31
  3. instance OAI.WeakPureInfiniteness.(instance at line 34) line 34
  4. def OAI.WeakPureInfiniteness.principalRightMap line 37
  5. lemma OAI.WeakPureInfiniteness.principalRightMap_dense line 42
  6. lemma OAI.WeakPureInfiniteness.norm_mul_abs line 50
  7. def OAI.WeakPureInfiniteness.partialPolar line 62
  8. lemma OAI.WeakPureInfiniteness.partialPolar_apply_mul line 65
  9. lemma OAI.WeakPureInfiniteness.partialPolar_norm line 72
  10. lemma OAI.WeakPureInfiniteness.partialPolar_initial_square line 80
  11. lemma OAI.WeakPureInfiniteness.partialPolar_mem_rightIdeal line 93
  12. def OAI.WeakPureInfiniteness.sandwichSubalgebra line 101
  13. def OAI.WeakPureInfiniteness.hereditarySubalgebra line 117
  14. instance OAI.WeakPureInfiniteness.(instance at line 120) line 120
  15. instance OAI.WeakPureInfiniteness.(instance at line 124) line 124
  16. lemma OAI.WeakPureInfiniteness.sandwich_mem line 128
  17. lemma OAI.WeakPureInfiniteness.square_mem_hereditary line 131
  18. lemma OAI.WeakPureInfiniteness.sqrt_mem_hereditary line 138
  19. lemma OAI.WeakPureInfiniteness.self_mem_hereditary line 144
  20. lemma OAI.WeakPureInfiniteness.principalRightIdeal_mul_mem line 151
  21. lemma OAI.WeakPureInfiniteness.hereditary_le_rightIdeal line 160
  22. lemma OAI.WeakPureInfiniteness.rightIdeal_square_mem_hereditary line 167
  23. def OAI.WeakPureInfiniteness.residual line 177
  24. lemma OAI.WeakPureInfiniteness.residual_nonneg line 179
  25. lemma OAI.WeakPureInfiniteness.residual_mono line 188
  26. lemma OAI.WeakPureInfiniteness.residual_square line 196
  27. lemma OAI.WeakPureInfiniteness.norm_sub_left_mul_sq_le line 201
  28. lemma OAI.WeakPureInfiniteness.norm_residual_le line 209
  29. lemma OAI.WeakPureInfiniteness.norm_sub_left_mul_le_sqrt line 221
  30. lemma OAI.WeakPureInfiniteness.principalRightIdeal_of_square_le line 226
  31. lemma OAI.WeakPureInfiniteness.mem_hereditary_of_le line 253
  32. lemma OAI.WeakPureInfiniteness.principalRightIdeal_le_of_mem line 262
  33. lemma OAI.WeakPureInfiniteness.principalRightIdeal_smul_le line 270
  34. lemma OAI.WeakPureInfiniteness.principalRightIdeal_of_square_le_smul line 279
  35. lemma OAI.WeakPureInfiniteness.mem_hereditary_of_le_smul line 284
  36. lemma OAI.WeakPureInfiniteness.principalRightIdeal_sqrt line 293
  37. lemma OAI.WeakPureInfiniteness.exists_exact_initial_square_of_domination line 304
  38. lemma OAI.WeakPureInfiniteness.exists_exact_initial_square_in_hereditary line 323
  39. lemma OAI.WeakPureInfiniteness.exists_comparison_of_rightIdeal line 331
  40. lemma OAI.WeakPureInfiniteness.exists_comparison_of_hereditary line 353
  41. lemma OAI.WeakPureInfiniteness.exists_comparison_of_star_mul line 362