eapprox — Mathlib

English

eapprox is the sequence of simple-function approximations of a function f: α → ENNReal, defined via ennrealRatEmbed.

Русский

eapprox — последовательность простых функций-аппроксимаций для f: α → ENNReal, определяемая через ennrealRatEmbed.

LaTeX

$$$\text{eapprox} = \text{approx}\;\text{ennrealRatEmbed}$$$

Lean4

/-- Approximate a function `α → ℝ≥0∞` by a sequence of simple functions. -/
def eapprox : (α → ℝ≥0∞) → ℕ → α →ₛ ℝ≥0∞ :=
  approx ennrealRatEmbed

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