fiberwise_right — Mathlib

English

If a function f on α×β is Theta to g on l×l' then for almost every fixed y in l' the slices f(·, y) and g(·, y) are Theta with respect to l.

Русский

Если функция f на α×β является Θ относительно l×l', то для почти всех фиксированных y в l' срезы f(·, y) и g(·, y) удовлетворяют Θ относительно l.

LaTeX

$$$\forall f,g: \alpha\times\beta \to E:\; f =Θ[l\times^s l'] g \Rightarrow (\forall \text{ almost all } y\in l',\; f(·,y)=Θ_l g(·,y))$$$

Lean4

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

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