analyticWithinAt — Mathlib

English

If a function f: E → F is analytic at a point x ∈ E, then f is analytic within every subset s ⊆ E at x.

Русский

Если функция f: E → F аналитична в точке x ∈ E, то она аналитична внутри любого подмножества s ⊆ E в точке x.

LaTeX

$$$\text{AnalyticAt}_{\mathcal{K}}(f,x) \Rightarrow \text{AnalyticWithinAt}_{\mathcal{K}}(f,s,x)$$$

Lean4

theorem analyticWithinAt (hf : AnalyticAt 𝕜 f x) : AnalyticWithinAt 𝕜 f s x :=
  by
  rw [← analyticWithinAt_univ] at hf
  apply hf.mono (subset_univ _)

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