English
For measurable f: γ → β, g: α → γ, and n, the n-th approximation commutes with composition: (approx i (f ∘ g) n) = (approx i f n) ∘ g.
Русский
Пусть f: γ → β и g: α → γ измеримы. Тогда для любого n аппроксимация по композиции совпадает: (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_apply [TopologicalSpace β] [OrderClosedTopology β] [MeasurableSpace β] [OpensMeasurableSpace β]
{i : ℕ → β} {f : α → β} {n : ℕ} (a : α) (hf : Measurable f) :
(approx i f n : α →ₛ β) a = (Finset.range n).sup fun k => if i k ≤ f a then i k else 0 :=
by
dsimp only [approx]
rw [finset_sup_apply]
congr
funext k
rw [restrict_apply]
· simp only [coe_const, mem_setOf_eq, indicator_apply, Function.const_apply]
· exact hf measurableSet_Ici
