restrict_le_zero_subset — Mathlib

English

If i is measurable and j ⊆ i, then v|_i ≤ 0 implies v|_j ≤ 0.

Русский

Если i измеримо и j ⊆ i, то если v|_i ≤ 0, тогда v|_j ≤ 0.

LaTeX

$$MeasurableSet(i) \to (j \subseteq i) \to (v \restriction i \le 0) \Rightarrow (v \restriction j \le 0)$$

Lean4

theorem restrict_le_zero_subset (hi₁ : MeasurableSet i) (hij : j ⊆ i) (hi₂ : v ≤[i] 0) : v ≤[j] 0 :=
  restrict_le_restrict_of_subset_le _ _ fun _ hk₁ hk₂ =>
    (restrict_le_restrict_iff _ _ hi₁).1 hi₂ hk₁ (Set.Subset.trans hk₂ hij)

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