fiberwise_left — Mathlib

English

If f = o_{l×ˢl'} g, then for almost every a in l, the slice f{ fst := a, snd := · } = o_{l'} g{ fst := a, snd := · }.

Русский

Если f = o_{l×ˢl'} g, то почти для каждого a в l верна аналогичная малость по отношению к срезам.

LaTeX

$$$f =o[l \timesˢ l'] g \Rightarrow \forall^\infty a\in l, \; f{ fst := a, snd := · } =o[l'] g{ fst := a, snd := · }$$$

Lean4

protected theorem fiberwise_left : f =O[l ×ˢ l'] g → ∀ᶠ b in l', (f ⟨·, b⟩) =O[l] (g ⟨·, b⟩) :=
  by
  simp only [isBigO_iff, eventually_iff, mem_prod_iff]
  rintro ⟨c, t₁, ht₁, t₂, ht₂, ht⟩
  exact mem_of_superset ht₂ fun _ hb ↦ ⟨c, mem_of_superset ht₁ fun _ ha ↦ ht ⟨ha, hb⟩⟩

Похожие утверждения