congr_mono — Mathlib

English

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

Русский

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

LaTeX

$$$ (ContinuousWithinAt f s x) \land (∀ y∈s1, g(y)=f(y)) \land (s1\subseteq s) \Rightarrow (ContinuousWithinAt g s1 x).$$$

Lean4

theorem congr_mono (h : ContinuousWithinAt f s x) (h' : EqOn g f s₁) (h₁ : s₁ ⊆ s) (hx : g x = f x) :
    ContinuousWithinAt g s₁ x :=
  (h.mono h₁).congr h' hx

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