rnDeriv_ne_top — Mathlib

English

For finite kernels κ and η and any a, rnDeriv κ η a x ≠ ∞ holds almost everywhere with respect to η a.

Русский

Для конечных ядер κ и η и любого a, rnDeriv κ η a x не бесконечна почти всюду относительно η a.

LaTeX

$$∀ᵐ x ∂(η a), rnDeriv κ η a x ≠ ∞$$

Lean4

theorem rnDeriv_ne_top (κ η : Kernel α γ) [IsFiniteKernel κ] [IsFiniteKernel η] {a : α} :
    ∀ᵐ x ∂(η a), rnDeriv κ η a x ≠ ∞ := by filter_upwards [κ.rnDeriv_lt_top η] with a h using h.ne

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