top_apply — Mathlib

English

For any nonempty set s, the top outer measure evaluates to infinity on s: ⊤ s = ∞.

Русский

Для любой непустой множества s верхняя внешняя мера равна бесконечности: ⊤ s = ∞.

LaTeX

$$$ (\top : OuterMeasure\ α)\ s = \infty $$$

Lean4

@[simp]
theorem top_apply {s : Set α} (h : s.Nonempty) : (⊤ : OuterMeasure α) s = ∞ :=
  let ⟨a, as⟩ := h
  top_unique <| le_trans (by simp [smul_dirac_apply, as]) (le_iSup₂ (∞ • dirac a) trivial)

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