restrict_mono — Mathlib

English

If s ⊆ t and m ≤ m' then restrict s m ≤ restrict t m'.

Русский

Если s ⊆ t и m ≤ m', тогда restrict s m ≤ restrict t m'.

LaTeX

$$$ s \subseteq t \Rightarrow m \le m' \Rightarrow (\restrict\ s\ m) \le (\restrict\ t\ m') $$$

Lean4

@[mono]
theorem restrict_mono {s t : Set α} (h : s ⊆ t) {m m' : OuterMeasure α} (hm : m ≤ m') : restrict s m ≤ restrict t m' :=
  fun u => by
  simp only [restrict_apply]
  exact (hm _).trans (m'.mono <| inter_subset_inter_right _ h)

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