restrict_le_restrict_subset — Mathlib

English

If i ⊆ i', and v|i ≤ w|i' (in the restricted sense), then v|j ≤ w|j for all j ⊆ i.

Русский

Если i ⊆ i' и v|i ≤ w|i' (в ограниченном смысле), тогда v|j ≤ w|j для всех j ⊆ i.

LaTeX

$$$ v \\restriction i ≤[j] w \\restriction j \\text{ for all } j ⊆ i $$$

Lean4

theorem restrict_le_restrict_subset {i j : Set α} (hi₁ : MeasurableSet i) (hi₂ : v ≤[i] w) (hij : j ⊆ i) : v ≤[j] w :=
  restrict_le_restrict_of_subset_le v w fun _ _ hk₂ =>
    subset_le_of_restrict_le_restrict v w hi₁ hi₂ (Set.Subset.trans hk₂ hij)

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