OAI/Analysis/MarkovType/SeminormUniformApproximation.lean
2 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.MarkovSuperreflexivity.SeminormApproximation.continuous_of_norm_boundline 18 - theorem
OAI.MarkovSuperreflexivity.SeminormApproximation.exists_relative_approximationline 26