OAI/Analysis/Cotype/QuotientLifts.lean
2 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.Cotype.quotient_lift_norm_ltline 14 - theorem
OAI.Cotype.quotient_lift_norm_le_twoline 51
OAI/Analysis/Cotype/QuotientLifts.lean2 declarations, 0 contain sorry, 0 declared as axioms
OAI.Cotype.quotient_lift_norm_lt line 14OAI.Cotype.quotient_lift_norm_le_two line 51