le_piecewise_of_le_of_le — Mathlib

English

If hf and hg express pointwise ≤ between f,g and f',g' respectively (with hf: ∀x∈s, f x ≤ f' x and hg: ∀x∉s, g x ≤ g' x), then s.piecewise f g ≤ s.piecewise f' g'.

Русский

Если hf и hg задают по точкам неравенства между f, f' и g, g' соответственно, тогда s.piecewise f g ≤ s.piecewise f' g'.

LaTeX

$$$$ (hf : \\forall x \\in s,\; f x \\le f' x) \\; (hg : \\forall x \\notin s,\; g x \\le g' x) \\Rightarrow s.piecewise f g \\le s.piecewise f' g'. $$$$

Lean4

theorem le_piecewise_of_le_of_le (hf : h ≤ f) (hg : h ≤ g) : h ≤ s.piecewise f g := fun x =>
  piecewise_cases s f g (fun y => h x ≤ y) (hf x) (hg x)

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