OAI/Probability/FreeIsing/Estimates/CountableProjective.lean
6 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.Problem367.CountableProjective.splitline 12 - lemma
OAI.Problem367.CountableProjective.split_measurableline 16 - lemma
OAI.Problem367.CountableProjective.split_injectiveline 20 - lemma
OAI.Problem367.CountableProjective.split_comp_restrictline 31 - theorem
OAI.Problem367.CountableProjective.exists_nat_marginalsline 37 - theorem
OAI.Problem367.CountableProjective.exists_nat_projective_limitline 78