measure_eq_left_of_subset_of_measure_add_eq

English

If (μ + ν)(t) ≠ ∞, s ⊆ t, and (μ + ν)(s) = (μ + ν)(t), then μ(s) = μ(t).

Русский

Если (μ+ν)(t) ≠ ∞, s ⊆ t и (μ+ν)(s) = (μ+ν)(t), то μ(s) = μ(t).

LaTeX

$$$\text{If } (μ+ν)(t) \neq ∞, \; s \subseteq t, \; (μ+ν)(s) = (μ+ν)(t) \Rightarrow μ(s) = μ(t).$$$

Lean4

theorem measure_eq_left_of_subset_of_measure_add_eq {s t : Set α} (h : (μ + ν) t ≠ ∞) (h' : s ⊆ t)
    (h'' : (μ + ν) s = (μ + ν) t) : μ s = μ t :=
  by
  refine le_antisymm (measure_mono h') ?_
  have : μ t + ν t ≤ μ s + ν t :=
    calc
      μ t + ν t = μ s + ν s := h''.symm
      _ ≤ μ s + ν t := by gcongr
  apply ENNReal.le_of_add_le_add_right _ this
  exact ne_top_of_le_ne_top h (le_add_left le_rfl)

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