restrict_le_restrict_of_subset_le

English

If i ⊆ j and v ≤[j] w, then v ≤[i] w.

Русский

Если i ⊆ j и v ≤[j] w, то v ≤[i] w.

LaTeX

$$$ i \\subseteq j \\Rightarrow v \\le[j] w \\Rightarrow v \\le[i] w $$$

Lean4

theorem restrict_le_restrict_of_subset_le {i : Set α} (h : ∀ ⦃j⦄, MeasurableSet j → j ⊆ i → v j ≤ w j) : v ≤[i] w :=
  by
  by_cases hi : MeasurableSet i
  · exact (restrict_le_restrict_iff _ _ hi).2 h
  · rw [restrict_not_measurable v hi, restrict_not_measurable w hi]

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