congr_of_insert — Mathlib

English

Let f,g: α→β and s⊆α with x∈s. If f is continuous within s at x and g equals f on insert x s, then g is continuous within s at x.

Русский

Пусть f,g: α→β и s⊆α с x∈s. Если f непрерывна на s в x и g совпадает с f на вставке x s, то g непрерывна на s в x.

LaTeX

$$$ (f\text{ continuous within } s\; x) \land (g =^{𝓝[\mathrm{insert}\ x\ s]} f) \Rightarrow (g\text{ continuous within } s\; x).$$$

Lean4

theorem congr_of_insert (h : ContinuousWithinAt f s x) (h₁ : ∀ y ∈ insert x s, g y = f y) : ContinuousWithinAt g s x :=
  h.congr (fun y hy ↦ h₁ y (mem_insert_of_mem _ hy)) (h₁ x (mem_insert _ _))

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