le_pre — Mathlib

English

Continuity from above: the measure of the intersection of a sequence of measurable sets equals the infimum of the measures of the finite intersections.

Русский

Переход сверху: мера пересечения последовательности измеримых множеств равна инфимууму меры частичных пересечений.

LaTeX

$$$\\mu\\left(\\bigcap_{i} f(i)\\right) = \\inf_{i} \\mu\\left(\\bigcap_{j \\le i} f(j)\\right)$$$

Lean4

theorem le_pre : μ ≤ pre m r ↔ ∀ s : Set X, diam s ≤ r → μ s ≤ m s := by
  simp only [pre, le_boundedBy, extend, le_iInf_iff]

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