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]