restrict_mono — Mathlib

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]

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