OAI/Analysis/AffineBernstein/RoundSliceContractions.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.AffineBernstein.dirDeriv_prod_rightline 17 - lemma
OAI.AffineBernstein.flatInverseTrace_prod_rightline 24 - lemma
OAI.AffineBernstein.flatInversePair_prod_rightline 32 - lemma
OAI.AffineBernstein.supportNewtonTrace_sliceline 40 - lemma
OAI.AffineBernstein.supportNewtonPair_sliceline 67