congr_mono — Mathlib

English

If f is ContDiffOn 𝕜 n f s, f1 agrees with f on s1, and s1 ⊆ s, then f1 is ContDiffOn 𝕜 n on s1 (constructed via monotonicity and congruence).

Русский

Если f ∈ ContDiffOn 𝕜 n f s, f1 совпадает с f на s1 и s1 ⊆ s, тогда f1 ∈ ContDiffOn 𝕜 n f s1.

LaTeX

$$$ContDiffOn\\ 𝕜\\ n\\ f\\ s\\rightarrow(∀x∈s_1\\, f_1 x=f x)\\rightarrow s_1\\subseteq s\\rightarrow ContDiffOn\\ 𝕜\\ n\\ f_1\\ s_1$$$

Lean4

theorem congr_mono (hf : ContDiffOn 𝕜 n f s) (h₁ : ∀ x ∈ s₁, f₁ x = f x) (hs : s₁ ⊆ s) : ContDiffOn 𝕜 n f₁ s₁ :=
  (hf.mono hs).congr h₁

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