piecewise_le_of_le_of_le

Mathlib.Data.Finset.Piecewise

URI: https://scilib.ai/kg/mathlib#Finset.piecewise_le_of_le_of_le

English

If f ≤ h and g ≤ h (pointwise), then s.piecewise f g ≤ h.

Русский

Если f ≤ h и g ≤ h по каждому аргументу, то s.piecewise f g ≤ h.

LaTeX

$$$$\\bigl(f \\le h\\bigr) \\land\\bigl(g \\le h\\bigr) \\Rightarrow s.piecewise f g \\le h.$$$$

Lean4

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

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru