isComplete_aestronglyMeasurable — Mathlib

English

The set of AEStronglyMeasurable[m] functions in Lp is complete; in particular, the subtype is complete under the induced topology.

Русский

Множество AEStronglyMeasurable[m]-функций в Lp является полным; в частности подмножество полно относительно индуцированной топологии.

LaTeX

$$$\text{IsComplete} (\{f:\ Lp F p μ \mid AEStronglyMeasurable[m] f μ\})$$$

Lean4

theorem isComplete_aestronglyMeasurable [hp : Fact (1 ≤ p)] [CompleteSpace F] (hm : m ≤ m0) :
    IsComplete {f : Lp F p μ | AEStronglyMeasurable[m] f μ} :=
  by
  rw [← completeSpace_coe_iff_isComplete]
  haveI : Fact (m ≤ m0) := ⟨hm⟩
  change CompleteSpace (lpMeasSubgroup F m p μ)
  infer_instance

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