OAI/Combinatorics/Progressions/Sampling/PrecenterForecastNativeAtomDictionary.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.FiniteProbabilityWeights.sampledComplexTest line 10
2. theorem OAI.Erdos3.exists_precenter_forecast_finiteLaw_native_partners line 24
3. abbrev OAI.Erdos3.PrecenterForecastNativeAtomLabel line 123
4. instance OAI.Erdos3.precenterForecastNativeAtomLabelFintype line 127
5. theorem OAI.Erdos3.precenterForecastNativeAtomLabel_card_le line 133
6. structure OAI.Erdos3.PrecenterForecastNativeAtomDictionary line 146
7. theorem OAI.Erdos3.exists_precenterForecastNativeAtomDictionary line 157
8. theorem OAI.Erdos3.exists_precenter_forecast_finiteLaw_native_atom_labels line 178