mono — Mathlib

English

If an analytic condition holds on s, it holds on any t ⊆ s within nhds.

Русский

Если аналитическое условие верно на s, то верно на любом подмножестве t ⊆ s в nhds.

LaTeX

$$AnalyticWithinAt 𝕜 f s x \\rightarrow t ⊆ s \\Rightarrow AnalyticWithinAt 𝕜 f t x$$

Lean4

theorem mono (hf : AnalyticWithinAt 𝕜 f s x) (h : t ⊆ s) : AnalyticWithinAt 𝕜 f t x :=
  by
  obtain ⟨p, hp⟩ := hf
  exact ⟨p, hp.mono h⟩

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