closure_subset_measurableSet — Mathlib

English

If K is compact in an R1 space and s ⊆ γ is measurable with K ⊆ s, then closure(K) ⊆ s.

Русский

Если K компактно в пространстве R1 и s ⊆ γ измеримо и K ⊆ s, то closure(K) ⊆ s.

LaTeX

$$$\\text{If } K \\subset \\gamma \\text{ is compact and } s \\subset \\gamma \\text{ is measurable with } K \\subset s \\Rightarrow \\overline{K} \\subset s.$$$

Lean4

/-- If `K` is a compact set in an R₁ space and `s ⊇ K` is a Borel measurable superset,
then `s` includes the closure of `K` as well. -/
theorem closure_subset_measurableSet [R1Space γ] {K s : Set γ} (hK : IsCompact K) (hs : MeasurableSet s) (hKs : K ⊆ s) :
    closure K ⊆ s := by
  rw [hK.closure_eq_biUnion_inseparable, iUnion₂_subset_iff]
  exact fun x hx y hy ↦ (hy.mem_measurableSet_iff hs).1 (hKs hx)

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