piecewise_mem_Icc_of_mem_of_mem — Mathlib

English

If f,g,f',g' lie in Set.Icc f' g' (i.e., f' ≤ f ≤ g' and f' ≤ g ≤ g'), then s.piecewise f g lies in Set.Icc f' g'.

Русский

Если f,g,f',g' принадлежат интервалу Icc f' g', тогда s.piecewise f g принадлежит Icc f' g'.

LaTeX

$$$$ \\text{If } f, g, f', g' \\in \\mathrm{Set.Icc}\\ f'\\ g', \\; s.piecewise f g \\in \\mathrm{Set.Icc}\\ f'\\ g'. $$$$

Lean4

theorem piecewise_mem_Icc_of_mem_of_mem (hf : f ∈ Set.Icc f' g') (hg : g ∈ Set.Icc f' g') :
    s.piecewise f g ∈ Set.Icc f' g' :=
  ⟨le_piecewise_of_le_of_le _ hf.1 hg.1, piecewise_le_of_le_of_le _ hf.2 hg.2⟩

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