English
If f ≤ g pointwise as simple functions, then restricting to any set s preserves the inequality: f.restrict s ≤ g.restrict s.
Русский
Если f(x) ≤ g(x) для всех x, то при ограничении к любому множеству s выполняется f|s ≤ g|s.
LaTeX
$$$ f \le g \quad\Rightarrow\quad f.restrict s \le g.restrict s $$$
Lean4
@[gcongr, mono]
theorem restrict_mono [Preorder β] (s : Set α) {f g : α →ₛ β} (H : f ≤ g) : f.restrict s ≤ g.restrict s :=
if hs : MeasurableSet s then fun x => by simp only [coe_restrict _ hs, indicator_le_indicator (H x)]
else by simp only [restrict_of_not_measurable hs, le_refl]