congr_mono — Mathlib

English

If f and f1 agree on s, then ContMDiffOn I I' n f s ↔ ContMDiffOn I I' n f1 s.

Русский

Если f1 совпадает с f на s, то ContMDiffOn I I' n f s эквивалентно ContMDiffOn I I' n f1 s.

LaTeX

$$$ (\forall y, f1 y = f y) \Rightarrow ContMDiffOn I I' n f1 s \iff ContMDiffOn I I' n f s$$

Lean4

theorem congr_mono (hf : ContMDiffOn I I' n f s) (h₁ : ∀ y ∈ s₁, f₁ y = f y) (hs : s₁ ⊆ s) : ContMDiffOn I I' n f₁ s₁ :=
  (hf.mono hs).congr h₁

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