subset — Mathlib

English

For any S, IsTightMeasureSet S is equivalent to the statement that for all ε > 0 there exists a compact K with μ(K^c) ≤ ε for all μ ∈ S.

Русский

Для любого S эквивалентно: существует компактное K такое, что для всех μ ∈ S μ(K^c) ≤ ε.

LaTeX

$$IsTightMeasureSet(S) ↔ ∀ ε > 0, ∃ K IsCompact such that ∀ μ ∈ S, μ(K^c) ≤ ε$$

Lean4

protected theorem subset (hT : IsTightMeasureSet T) (hST : S ⊆ T) : IsTightMeasureSet S :=
  tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds hT (fun _ ↦ by simp) (iSup_le_iSup_of_subset hST)

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