English
If f1 ≤ g1 on s and f2 ≤ g2 on sᶜ, then s.piecewise f1 f2 ≤ s.piecewise g1 g2 pointwise.
Русский
Если f1 ≤ g1 на s и f2 ≤ g2 на sᶜ, тогда по точкам s.piecewise f1 f2 ≤ s.piecewise g1 g2.
LaTeX
$$$\\forall i,\\ (i\\in s \\Rightarrow f_1(i) \\le g_1(i)) \\land (i\\notin s \\Rightarrow f_2(i) \\le g_2(i)) \\Rightarrow (s.\\mathrm{piecewise} f_1 f_2)(i) \\le (s.\\mathrm{piecewise} g_1 g_2)(i)$$$
Lean4
@[gcongr]
theorem piecewise_mono {δ : α → Type*} [∀ i, Preorder (δ i)] {s : Set α} [∀ j, Decidable (j ∈ s)]
{f₁ f₂ g₁ g₂ : ∀ i, δ i} (h₁ : ∀ i ∈ s, f₁ i ≤ g₁ i) (h₂ : ∀ i ∉ s, f₂ i ≤ g₂ i) :
s.piecewise f₁ f₂ ≤ s.piecewise g₁ g₂ := by apply piecewise_le <;> intros <;> simp [*]
