congr_mono — Mathlib

English

If s ⊆ t and f is continuous on t, then f is continuous on s.

Русский

Если s ⊆ t и f непрерывна на t, тогда f непрерывна на s.

LaTeX

$$$$s \subseteq t \Rightarrow (\text{ContinuousOn}(f,t) \Rightarrow \text{ContinuousOn}(f,s)).$$$$

Lean4

theorem congr_mono (h : ContinuousOn f s) (h' : EqOn g f s₁) (h₁ : s₁ ⊆ s) : ContinuousOn g s₁ :=
  by
  intro x hx
  unfold ContinuousWithinAt
  have A := (h x (h₁ hx)).mono h₁
  unfold ContinuousWithinAt at A
  rw [← h' hx] at A
  exact A.congr' h'.eventuallyEq_nhdsWithin.symm

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