approxOn_mem — Mathlib

English

For any x, the approximant F_n(x) takes its values inside the target set s; i.e., F_n(·) maps into s for all n.

Русский

Для каждого x аппроксимация F_n(x) принимает значения внутри множества s; то есть F_n(·) отображается в s на всех n.

LaTeX

$$$\\forall x,\\; (approxOn\\; f\\; hf\\; s\\; y_0\\; h_0\\; n)\\; x \\in s.$$$

Lean4

theorem approxOn_mem {f : β → α} (hf : Measurable f) {s : Set α} {y₀ : α} (h₀ : y₀ ∈ s) [SeparableSpace s] (n : ℕ)
    (x : β) : approxOn f hf s y₀ h₀ n x ∈ s :=
  by
  haveI : Nonempty s := ⟨⟨y₀, h₀⟩⟩
  suffices ∀ n, (Nat.casesOn n y₀ ((↑) ∘ denseSeq s) : α) ∈ s by apply this
  rintro (_ | n)
  exacts [h₀, Subtype.mem _]

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