continuousWithinAt — Mathlib

English

If f is continuous on s and g agrees with f on s₁ ⊆ s, then g is continuous on s₁.

Русский

Если f непрерывна на s и g совпадает с f на подмножестве s₁ ⊆ s, то g непрерывна на s₁.

LaTeX

$$$$\text{ContinuousOn}(f,s) \to (\text{EqOn}(g,f,s_1) \land s_1 \subseteq s) \Rightarrow \text{ContinuousOn}(g,s_1)$$$$

Lean4

theorem continuousWithinAt (h : ContinuousAt f x) : ContinuousWithinAt f s x :=
  ContinuousWithinAt.mono ((continuousWithinAt_univ f x).2 h) (subset_univ _)

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