OAI/Combinatorics/BalancedRyser/Profiles/ProfileAmbientCompactness.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Balanced.ProfileAmbientCompactness.boundedProfiles_eq line 11
  2. theorem OAI.Balanced.ProfileAmbientCompactness.isCompact_boundedProfiles line 18
  3. theorem OAI.Balanced.ProfileAmbientCompactness.isClosed_boundedProfiles line 23
  4. theorem OAI.Balanced.ProfileAmbientCompactness.boundedProfile_of_tendsto line 27
  5. theorem OAI.Balanced.ProfileAmbientCompactness.compact_support_of_tendsto line 33
  6. theorem OAI.Balanced.ProfileAmbientCompactness.boundedProfile_support_of_tendsto line 50
  7. theorem OAI.Balanced.ProfileAmbientCompactness.ae_boundedProfile_of_tendsto line 57
  8. theorem OAI.Balanced.ProfileAmbientCompactness.map_comap_subtype line 66
  9. theorem OAI.Balanced.ProfileAmbientCompactness.map_subtype_support line 77
  10. theorem OAI.Balanced.ProfileAmbientCompactness.nonempty_boundedProfiles line 85
  11. theorem OAI.Balanced.ProfileAmbientCompactness.exists_ambient_profile_measure_subsequence line 90
  12. theorem OAI.Balanced.ProfileAmbientCompactness.exists_full_ambient_profile_subsequence line 115