piecewise_mem_Icc — Mathlib

English

If f ≤ g, then s.piecewise f g lies in the closed interval between f and g: f ≤ s.piecewise f g ≤ g.

Русский

Если f ≤ g, то s.piecewise f g принадлежит замкнутому отрезку [f,g]: f ≤ s.piecewise f g ≤ g.

LaTeX

$$$$\\text{If } f \\le g,\\quad s.piecewise f g \\in \\mathrm{Icc}\\ f\\ g.$$$$

Lean4

theorem piecewise_mem_Icc (h : f ≤ g) : s.piecewise f g ∈ Set.Icc f g :=
  piecewise_mem_Icc_of_mem_of_mem _ (Set.left_mem_Icc.2 h) (Set.right_mem_Icc.2 h)

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