approx_comp — Mathlib

English

If f: γ → β and g: α → γ are measurable, then the n-th approximation of f ∘ g equals the n-th approximation of f composed with g: (approx i (f ∘ g) n) = (approx i f n) ∘ g.

Русский

Если f: γ → β и g: α → γ измеримы, то аппроксимация композиции равна композиции аппроксимации: (approx i (f ∘ g) n) = (approx i f n) ∘ g.

LaTeX

$$$ (approx\ i\ (f \circ g)\ n) = (approx\ i\ f\ n) \circ g $$$

Lean4

theorem approx_comp [TopologicalSpace β] [OrderClosedTopology β] [MeasurableSpace β] [OpensMeasurableSpace β]
    [MeasurableSpace γ] {i : ℕ → β} {f : γ → β} {g : α → γ} {n : ℕ} (a : α) (hf : Measurable f) (hg : Measurable g) :
    (approx i (f ∘ g) n : α →ₛ β) a = (approx i f n : γ →ₛ β) (g a) := by
  rw [approx_apply _ hf, approx_apply _ (hf.comp hg), Function.comp_apply]

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