instCompleteSpaceSubtypeAEEqFunMemAddSubgroupLpLpMeasSubgroupOfFactLeMeasurableSpace

English

Under mild hypotheses, the complete space structure passes to the subtype lpMeasSubgroup F m p μ when m ≤ m0 and 1 ≤ p.

Русский

При умеренных гипотезах полное пространство переходит к подмножеству lpMeasSubgroup при m ≤ m0 и 1 ≤ p.

LaTeX

$$$\text{CompleteSpace}(lpMeasSubgroup F m p μ)$$$

Lean4

instance [hm : Fact (m ≤ m0)] [CompleteSpace F] [hp : Fact (1 ≤ p)] : CompleteSpace (lpMeasSubgroup F m p μ) := by
  rw [(lpMeasSubgroupToLpTrimIso F p μ hm.elim).completeSpace_iff]; infer_instance

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