OAI/Probability/ClassicalON/FinFKG.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.ClassicalON.weightedMean_equivline 17 - theorem
OAI.ClassicalON.continuousFKG_equivline 23 - theorem
OAI.ClassicalON.continuousFKG_subsingletonline 40 - theorem
OAI.ClassicalON.continuousFKG_finline 58 - theorem
OAI.ClassicalON.continuousFKG_piline 86