integrableOn_compact_subset — Mathlib

English

A locally integrable function on s can be covered by countably many open sets, each where the function is integrable on the intersection with s.

Русский

Локально интегрируемая функция на s может быть покрыта счётной множ моей открытых множеств, на которых интегрируемость сохраняется на пересечении с s.

LaTeX

$$$\\exists T \\subseteq P(X)\\; (T\\text{ счетно}) \\land (\\forall u\\in T\\,\\text{IsOpen}(u)) \\,\\land \\, s \\subseteq \\bigcup_{u\\in T} u \\,\\land \\, \\forall u\\in T, \\text{IntegrableOn}(f, u\\cap s, μ)$$$

Lean4

theorem integrableOn_compact_subset [PseudoMetrizableSpace ε] (hf : LocallyIntegrableOn f s μ) {t : Set X} (hst : t ⊆ s)
    (ht : IsCompact t) : IntegrableOn f t μ :=
  (hf.mono_set hst).integrableOn_isCompact ht

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