le_boundedBy — Mathlib

English

For any μ ∈ OuterMeasure α, μ ≤ boundedBy m if and only if μ(s) ≤ m(s) for all s.

Русский

Для всякой μ ∈ OuterMeasure α верно μ ≤ boundedBy m тогда и только тогда, когда μ(s) ≤ m(s) для всех s.

LaTeX

$$$\\mu \\leq \\mathrm{boundedBy}(m) \\iff \\forall s, \\mu(s) \\le m(s)$$$

Lean4

theorem le_boundedBy {μ : OuterMeasure α} : μ ≤ boundedBy m ↔ ∀ s, μ s ≤ m s :=
  by
  rw [boundedBy, le_ofFunction, forall_congr']; intro s
  rcases s.eq_empty_or_nonempty with h | h <;> simp [h, Set.not_nonempty_empty]

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