subset_le_of_restrict_le_restrict

English

If ∀ j ⊆ i with MeasurableSet j, v j ≤ w j, then v ≤[i] w.

Русский

Если для всех j ⊆ i с MeasurableSet j выполняется v j ≤ w j, то v ≤[i] w.

LaTeX

$$$ \\Bigl( \\forall j \\subseteq i, MeasurableSet(j) \\Rightarrow v(j) \\le w(j) \\Bigr) \\Rightarrow v \\le[i] w $$$

Lean4

theorem subset_le_of_restrict_le_restrict {i : Set α} (hi : MeasurableSet i) (hi₂ : v ≤[i] w) {j : Set α} (hj : j ⊆ i) :
    v j ≤ w j := by
  by_cases hj₁ : MeasurableSet j
  · exact (restrict_le_restrict_iff _ _ hi).1 hi₂ hj₁ hj
  · rw [v.not_measurable hj₁, w.not_measurable hj₁]

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