continuousWithinAt_congr_of_insert

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{ ContinuousWithinAt } s x) \land (g =^{𝓝[\mathrm{insert}\ x\ s]} f) \Rightarrow (ContinuousWithinAt g s x).$$$

Lean4

theorem continuousWithinAt_congr_of_insert (h₁ : ∀ y ∈ insert x s, g y = f y) :
    ContinuousWithinAt g s x ↔ ContinuousWithinAt f s x :=
  continuousWithinAt_congr (fun y hy ↦ h₁ y (mem_insert_of_mem _ hy)) (h₁ x (mem_insert _ _))

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