OAI/Analysis/BernoulliCone/CompactZeroFiber.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Bernoulli.Foliation.eventually_near_zero_fiber line 14

   Source documentation

   Compact zero-fiber control. No convergence of the selected root is needed.

   lemma eventually_near_zero_fiber {K:Set E} (hK:IsCompact K) {f g:E→ℝ} {C:ℝ}
       (hf:∀x∈K,ContinuousAt f x) (hg:∀x∈K,ContinuousAt g x)
       (hzero:∀x∈K,f x=0 → g x<C) :
       ∀ᶠ t:ℝ in 𝓝 0,∀x∈K,f x=t → g x<C := by
   …