OAI/Probability/CriticalPercolation/ProductMeasure/CoordinateNeDensity.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.CriticalPercolation.FiniteProduct.coordinate_ne_zero_of_densityline 18 - lemma
OAI.CriticalPercolation.FiniteProduct.density_force_nonzeroline 22 - lemma
OAI.CriticalPercolation.FiniteProduct.density_pin_of_supportline 34 - lemma
OAI.CriticalPercolation.FiniteProduct.delta_congr_supportline 41 - lemma
OAI.CriticalPercolation.FiniteProduct.openPivot_congr_supportline 49