le_boundedBy' — Mathlib

English

A variant: μ ≤ boundedBy m is equivalent to ∀ s, s.Nonempty → μ s ≤ m s.

Русский

Вариант: μ ≤ boundedBy m эквивалентно ∀ s, s.Nonempty → μ s ≤ m s.

LaTeX

$$$\\mu \\leq \\mathrm{boundedBy}(m) \\iff \\forall s: Set\\alpha, s.Nonempty \\rightarrow \\mu(s) \\le m(s)$$$

Lean4

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

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