OAI/SetTheory/PartitionPrinciple/Geometry/GroundMixtureDensityRecovery.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PartitionPilot.Forcing.TransitiveGround.niceNameCandidates_valid line 12
  2. def OAI.PartitionPilot.Forcing.TransitiveGround.niceVisibilityName line 19
  3. theorem OAI.PartitionPilot.Forcing.TransitiveGround.niceVisibilityName_code line 22
  4. theorem OAI.PartitionPilot.Forcing.TransitiveGround.entry_niceVisibilityName line 27
  5. theorem OAI.PartitionPilot.Forcing.TransitiveGround.mem_eval_niceVisibilityName line 33
  6. theorem OAI.PartitionPilot.Forcing.TransitiveGround.niceVisibilityName_mem line 39
  7. theorem OAI.PartitionPilot.Forcing.TransitiveGround.niceVisibilityName_support line 56
  8. theorem OAI.PartitionPilot.Forcing.TransitiveGround.niceVisibilityName_hs line 62
  9. theorem OAI.PartitionPilot.Forcing.TransitiveGround.niceVisibilityName_principal_hs line 72
  10. theorem OAI.PartitionPilot.Forcing.TransitiveGround.act_niceVisibilityName line 82
  11. theorem OAI.PartitionPilot.Forcing.TransitiveGround.mix_mem_mixtureCandidates line 106
  12. theorem OAI.PartitionPilot.Forcing.TransitiveGround.mixture_candidate_data line 120
  13. theorem OAI.PartitionPilot.Forcing.TransitiveGround.mixture_visibility_mem line 138
  14. theorem OAI.PartitionPilot.Forcing.TransitiveGround.mixture_visibility_hs line 152
  15. theorem OAI.PartitionPilot.Forcing.TransitiveGround.forcesMem_mixtureVisibility_of_dense line 176
  16. theorem OAI.PartitionPilot.Forcing.TransitiveGround.exists_mixtureCandidate_of_dense line 189