mono_of_mem_nhdsWithin — Mathlib

English

Same as above: insertion-based congruence for ContDiffWithinAt.

Русский

То же: сопоставление по вставке для ContDiffWithinAt.

LaTeX

$$$\\forall h_1: \\forall y \\in \\text{insert } x s, f_1 y = f y \\Rightarrow ContDiffWithinAt 𝕜 n f_1 s x \\leftrightarrow ContDiffWithinAt 𝕜 n f s x$$$

Lean4

theorem mono_of_mem_nhdsWithin (h : ContDiffWithinAt 𝕜 n f s x) {t : Set E} (hst : s ∈ 𝓝[t] x) :
    ContDiffWithinAt 𝕜 n f t x := by
  match n with
  | ω =>
    obtain ⟨u, hu, p, H, H'⟩ := h
    exact ⟨u, nhdsWithin_le_of_mem (insert_mem_nhdsWithin_insert hst) hu, p, H, H'⟩
  | (n : ℕ∞) =>
    intro m hm
    rcases h m hm with ⟨u, hu, p, H⟩
    exact ⟨u, nhdsWithin_le_of_mem (insert_mem_nhdsWithin_insert hst) hu, p, H⟩

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