boundedBy_eq — Mathlib

English

If ∅ is mapped to 0 by m, and m is monotone and subadditive on unions, then for all s we have boundedBy m s = m s.

Русский

Если ∅ обрабатывается как 0 и m монотона и подаддитивна по объединениям, тогда для всех s выполняется boundedBy m s = m s.

LaTeX

$$$\\text{boundedBy } m s = m s$$$

Lean4

theorem boundedBy_eq (s : Set α) (m_empty : m ∅ = 0) (m_mono : ∀ ⦃t : Set α⦄, s ⊆ t → m s ≤ m t)
    (m_subadd : ∀ s : ℕ → Set α, m (⋃ i, s i) ≤ ∑' i, m (s i)) : boundedBy m s = m s := by
  rw [boundedBy_eq_ofFunction m_empty, ofFunction_eq s m_mono m_subadd]

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