OAI/Combinatorics/RamseyFive/Streams/DependentPrivateStream.lean
4 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.SharpRamseyFive.FiniteEntropy.sigmaLaw_positiveline 11 - lemma
OAI.SharpRamseyFive.FiniteEntropy.map_sigma_firstline 15 - lemma
OAI.SharpRamseyFive.FiniteEntropy.sigma_streamline 21 - def
OAI.SharpRamseyFive.SelectedTuple.SelectedStream.augmentSigmaline 32