continuousOn — 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) \land (s_1 \subseteq s) \land \text{EqOn}(g,f,s_1) \Rightarrow \text{ContinuousOn}(g,s_1)$$$$

Lean4

@[fun_prop]
theorem continuousOn (h : Continuous f) : ContinuousOn f s :=
  by
  rw [← continuousOn_univ] at h
  exact h.mono (subset_univ _)

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