instSigmaFiniteRestrictInterSet_1

English

Let μ be a measure on α and s,t ⊆ α. If μ restricted to t is σ-finite, then μ restricted to s ∩ t is σ-finite.

Русский

Пусть μ — мера на α, и s,t ⊆ α. Если ограничение μ на t является σ-конечной мерой, то ограничение μ на s ∩ t также σ-конечно.

LaTeX

$$$\sigma\text{-finite}(\mu|_t) \implies \sigma\text{-finite}(\mu|_{s\cap t})$$$

Lean4

instance [SigmaFinite (μ.restrict t)] : SigmaFinite (μ.restrict (s ∩ t)) :=
  sigmaFinite_of_le (μ.restrict t) (restrict_mono_ae (ae_of_all _ Set.inter_subset_right))

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