fiberwise_left — Mathlib

English

If f =Θ[l×^s l'] g then for almost every y in l' the slices f(x, y) and g(x, y) are Θ with respect to l.

Русский

Если f =Θ[l×ˢl'] g, то для почти всех y ∈ l' срезы f(·, y) и g(·, y) удовлетворяют Θ относительно l.

LaTeX

$$$\forall f,g:\; f =Θ[l\timesˢ l'] g \Rightarrow (\forall \text{ a.e. } y\in l',\; f(\cdot,y)=Θ_l (g(\cdot,y)))$$$

Lean4

protected theorem fiberwise_left : f =Θ[l ×ˢ l'] g → ∀ᶠ y in l', (f ⟨·, y⟩) =Θ[l] (g ⟨·, y⟩) :=
  by
  simp only [IsTheta, eventually_and]
  exact fun ⟨h₁, h₂⟩ ↦ ⟨h₁.fiberwise_left, h₂.fiberwise_left⟩

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