boundedBy_apply — Mathlib

English

For any s, the value of boundedBy m on s is the infimum over all countable coverings t of s by sets, of the sum over n of the supremum (over nonempty subcollections) of m over t(n).

Русский

Для любого s значение boundedBy m на s равно инфимума над всеми счётными покрытиями t множества s суммой по n максимумов по не пустым подмножствам m на t(n).

LaTeX

$$$\\text{boundedBy } m\\, s = \\bigwedge_{t: \\mathbb{N} \\to Set\\alpha}\\; (s \\subseteq iUnion\\ t)\\;\\sum{'} n, \\bigl\\lceil \\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\bigsqcup _{:} (t n).Nonempty, m (t n) \\bigr\\rceil$$$

Lean4

theorem boundedBy_apply (s : Set α) :
    boundedBy m s = ⨅ (t : ℕ → Set α) (_ : s ⊆ iUnion t), ∑' n, ⨆ _ : (t n).Nonempty, m (t n) := by
  simp [boundedBy, ofFunction_apply]

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