zero_le_restrict_subset — Mathlib

English

If i is measurable and j ⊆ i, then nonnegativity on i implies nonnegativity on j.

Русский

Если i измеримо и j ⊆ i, то неотрицательность на i приводит к неотрицательности на j.

LaTeX

$$MeasurableSet(i) \to (j \subseteq i) \to (0 \le_i v) \Rightarrow (0 \le_j v)$$

Lean4

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

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