OAI/Analysis/AffineBernstein/VarianceSeparation.lean
2 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.AffineBernstein.variance_lower_of_separated_setsline 16 - lemma
OAI.AffineBernstein.compact_sublevel_in_compactline 51