Theorems · Theorem · measure theory

HasOuterApproxClosed.exAppr

∀ {X : Type u_1} {inst : TopologicalSpace X} [self : HasOuterApproxClosed X] (F : Set X),
  IsClosed F →
    ∃ fseq,
      (∀ (n : ℕ) (x : X), (fseq n) x ≤ 1) ∧
        (∀ (n : ℕ), ∀ x ∈ F, 1 ≤ (fseq n) x) ∧
          Filter.Tendsto (fun n x => (fseq n) x) Filter.atTop (nhds (F.indicator fun x => 1))

Defined in

Mathlib.MeasureTheory.Measure.HasOuterApproxClosed

Cited by

3 results in Mathlib

Foundations

Depth 120 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

HasOuterApproxClosed