OAI/Combinatorics/SharpRamsey/Learning/FiniteHeaderUnion.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SharpLogRamsey.PublicFamilies.union_log_bound line 11
2. lemma OAI.SharpLogRamsey.PublicFamilies.card_le_ceil_exp line 29
3. lemma OAI.SharpLogRamsey.PublicFamilies.log_ceil_exp line 36