approxOn_comp — Mathlib

English

Approximating a composition equals composing the approximant: applying approxOn to f∘g with hf.comp hg yields the composition of approxOn f with g.

Русский

Аппроксимация для композиции равна композиции аппроксимации: approxOn (f∘g) hf hg = (approxOn f hf) ∘ g.

LaTeX

$$$approxOn (f\\circ g) (hf\\circ hg) s\\ y_0\\ h_0\\ n = (approxOn f hf s y_0 h_0 n) \\circ g\\ hg.$$$

Lean4

@[simp]
theorem approxOn_comp {γ : Type*} [MeasurableSpace γ] {f : β → α} (hf : Measurable f) {g : γ → β} (hg : Measurable g)
    {s : Set α} {y₀ : α} (h₀ : y₀ ∈ s) [SeparableSpace s] (n : ℕ) :
    approxOn (f ∘ g) (hf.comp hg) s y₀ h₀ n = (approxOn f hf s y₀ h₀ n).comp g hg :=
  rfl

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