boundedBy_le — Mathlib

English

Let μ be an outer measure and m a set function. Then μ ≤ boundedBy m if and only if for every set s, μ(s) ≤ m(s).

Русский

Пусть μ — внешняя мера, а m — функция на множествах. Тогда μ ≤ boundedBy m тогда и только тогда, когда для каждого множества s выполняется μ(s) ≤ m(s).

LaTeX

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

Lean4

theorem boundedBy_le (s : Set α) : boundedBy m s ≤ m s :=
  (ofFunction_le _).trans iSup_const_le

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