piecewise_mono — Mathlib

English

If f1 ≤ f2 on s and g1 ≤ g2 on the complement of s, then the piecewise function piecewise s hs f1 g1 is ≤ piecewise s hs f2 g2.

Русский

Если f1 ≤ f2 на множестве s и g1 ≤ g2 на дополнении s, то функция piecewise s hs f1 g1 меньше или равна piecewise s hs f2 g2.

LaTeX

$$$piecewise s hs f_1 g_1 \\le piecewise s hs f_2 g_2\\quad\\text{если } f_1(a) \\le f_2(a)\\ (a \\in s),\\; g_1(a) \\le g_2(a)\\ (a \\notin s).$$$

Lean4

@[gcongr]
theorem piecewise_mono (hf : ∀ a ∈ s, f₁ a ≤ f₂ a) (hg : ∀ a ∉ s, g₁ a ≤ g₂ a) :
    piecewise s hs f₁ g₁ ≤ piecewise s hs f₂ g₂ :=
  Set.piecewise_mono hf hg

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