measure_diff_eq_top — Mathlib

English

If s has finite measure and t has infinite measure, then μ(s \\ t) = ∞.

Русский

Если μ(s) < ∞ и μ(t) = ∞, то μ(s \\ t) = ∞.

LaTeX

$$$$\\forall s,t:\\mathrm Set,\\; \\mu(s)=\\infty \\Rightarrow \\mu(t)\\ne \\infty \\Rightarrow \\mu(s\\setminus t)=\\infty.$$$$

Lean4

theorem measure_diff_eq_top (hs : μ s = ∞) (ht : μ t ≠ ∞) : μ (s \ t) = ∞ :=
  by
  contrapose! hs
  exact
    ((measure_mono (subset_diff_union s t)).trans_lt
        ((measure_union_le _ _).trans_lt (ENNReal.add_lt_top.2 ⟨hs.lt_top, ht.lt_top⟩))).ne

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