congr_of_eventuallyEq — Mathlib

English

Immediate corollary: ContDiffWithinAt implies continuity.

Русский

Непосредственный вывод: ContDiffWithinAt влечет непрерывность.

LaTeX

$$$ ContDiffWithinAt 𝕜 n f s x \\Rightarrow ContinuousWithinAt f s x$$

Lean4

theorem congr_of_eventuallyEq (h : ContDiffWithinAt 𝕜 n f s x) (h₁ : f₁ =ᶠ[𝓝[s] x] f) (hx : f₁ x = f x) :
    ContDiffWithinAt 𝕜 n f₁ s x := by
  match n with
  | ω =>
    obtain ⟨u, hu, p, H, H'⟩ := h
    exact
      ⟨{x ∈ u | f₁ x = f x}, Filter.inter_mem hu (mem_nhdsWithin_insert.2 ⟨hx, h₁⟩), p,
        (H.mono (sep_subset _ _)).congr fun _ ↦ And.right, fun i ↦ (H' i).mono (sep_subset _ _)⟩
  | (n : ℕ∞) =>
    intro m hm
    let ⟨u, hu, p, H⟩ := h m hm
    exact
      ⟨{x ∈ u | f₁ x = f x}, Filter.inter_mem hu (mem_nhdsWithin_insert.2 ⟨hx, h₁⟩), p,
        (H.mono (sep_subset _ _)).congr fun _ ↦ And.right⟩

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