piecewise_le_piecewise' — Mathlib

English

If hf : f ≤ f' and hg : g ≤ g', then s.piecewise f g ≤ s.piecewise f' g'.

Русский

Если f ≤ f' и g ≤ g', то s.piecewise f g ≤ s.piecewise f' g'.

LaTeX

$$$$ (hf : f \\le f') \\; (hg : g \\le g') \\Rightarrow s.piecewise f g \\le s.piecewise f' g'. $$$$

Lean4

theorem piecewise_le_piecewise' (hf : ∀ x ∈ s, f x ≤ f' x) (hg : ∀ x ∉ s, g x ≤ g' x) :
    s.piecewise f g ≤ s.piecewise f' g' := fun x => by by_cases hx : x ∈ s <;> simp [*]

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