restrict_le_restrict_iff — Mathlib

English

For a measurable i, v ≤[i] w holds iff for all measurable j ⊆ i, v j ≤ w j.

Русский

Для измеримого i верно v ≤[i] w тогда и только тогда, когда для всех измеримых j ⊆ i верно v j ≤ w j.

LaTeX

$$$ v \\le[ i ] w \\iff \\forall j, MeasurableSet(j) \\to j \\subseteq i \\to v(j) \\le w(j) $$$

Lean4

theorem restrict_le_restrict_iff {i : Set α} (hi : MeasurableSet i) :
    v ≤[i] w ↔ ∀ ⦃j⦄, MeasurableSet j → j ⊆ i → v j ≤ w j :=
  ⟨fun h j hj₁ hj₂ => restrict_eq_self v hi hj₁ hj₂ ▸ restrict_eq_self w hi hj₁ hj₂ ▸ h j hj₁, fun h =>
    le_iff.1 fun _ hj =>
      (restrict_apply v hi hj).symm ▸ (restrict_apply w hi hj).symm ▸ h (hj.inter hi) Set.inter_subset_right⟩

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