The actual supported subspace of ordinary spatial L²

Support is imposed on genuine Bochner L² functions by the closed kernel of identity minus measurable-set projection. This gives a complete Hilbert space for localized propagators and keeps the support restriction explicit.

noncomputable def EulerLpSupportedSubspace.cutoff {α : Type u_1} {V : Type u_2} [MeasurableSpace α] (μ : MeasureTheory.Measure α) [NormedAddCommGroup V] (S : Set α) (hS : MeasurableSet S) (u : ↥(MeasureTheory.Lp V 2 μ)) : ↥(MeasureTheory.Lp V 2 μ)

The actual measurable-set cutoff on a Bochner L² function.

Equations

• EulerLpSupportedSubspace.cutoff μ S hS u = MeasureTheory.MemLp.toLp (S.indicator ↑↑u) ⋯

theorem EulerLpSupportedSubspace.cutoff_ae {α : Type u_1} {V : Type u_2} [MeasurableSpace α] (μ : MeasureTheory.Measure α) [NormedAddCommGroup V] (S : Set α) (hS : MeasurableSet S) (u : ↥(MeasureTheory.Lp V 2 μ)) : ↑↑(cutoff μ S hS u) =ᵐ[μ] S.indicator ↑↑u

Its representative is the literal indicator product.

theorem EulerLpSupportedSubspace.cutoff_norm {α : Type u_1} {V : Type u_2} [MeasurableSpace α] (μ : MeasureTheory.Measure α) [NormedAddCommGroup V] (S : Set α) (hS : MeasurableSet S) (u : ↥(MeasureTheory.Lp V 2 μ)) : ‖cutoff μ S hS u‖ ≤ ‖u‖

Measurable-set projection is norm-decreasing.

noncomputable def EulerLpSupportedSubspace.cutoffLinear {α : Type u_1} {V : Type u_2} [MeasurableSpace α] (μ : MeasureTheory.Measure α) [NormedAddCommGroup V] [InnerProductSpace ℝ V] (S : Set α) (hS : MeasurableSet S) : ↥(MeasureTheory.Lp V 2 μ) →ₗ[ℝ] ↥(MeasureTheory.Lp V 2 μ)

The actual cutoff is linear.

Equations

• EulerLpSupportedSubspace.cutoffLinear μ S hS = { toFun := EulerLpSupportedSubspace.cutoff μ S hS, map_add' := ⋯, map_smul' := ⋯ }

noncomputable def EulerLpSupportedSubspace.cutoffOperator {α : Type u_1} {V : Type u_2} [MeasurableSpace α] (μ : MeasureTheory.Measure α) [NormedAddCommGroup V] [InnerProductSpace ℝ V] (S : Set α) (hS : MeasurableSet S) : ↥(MeasureTheory.Lp V 2 μ) →L[ℝ] ↥(MeasureTheory.Lp V 2 μ)

The supported-set projection as a genuine bounded linear map.

Equations

• EulerLpSupportedSubspace.cutoffOperator μ S hS = (EulerLpSupportedSubspace.cutoffLinear μ S hS).mkContinuous 1 ⋯

noncomputable def EulerLpSupportedSubspace.supportedSpace {α : Type u_1} {V : Type u_2} [MeasurableSpace α] (μ : MeasureTheory.Measure α) [NormedAddCommGroup V] [InnerProductSpace ℝ V] (S : Set α) (hS : MeasurableSet S) : Submodule ℝ ↥(MeasureTheory.Lp V 2 μ)

The localized Hilbert subspace is a closed kernel.

Equations

• EulerLpSupportedSubspace.supportedSpace μ S hS = (↑(ContinuousLinearMap.id ℝ ↥(MeasureTheory.Lp V 2 μ) - EulerLpSupportedSubspace.cutoffOperator μ S hS)).ker

theorem EulerLpSupportedSubspace.mem_supportedSpace_iff {α : Type u_1} {V : Type u_2} [MeasurableSpace α] (μ : MeasureTheory.Measure α) [NormedAddCommGroup V] [InnerProductSpace ℝ V] (S : Set α) (hS : MeasurableSet S) (u : ↥(MeasureTheory.Lp V 2 μ)) : u ∈ supportedSpace μ S hS ↔ u = cutoff μ S hS u

Membership is fixedness under actual measurable-set projection.

theorem EulerLpSupportedSubspace.mem_supportedSpace_ae {α : Type u_1} {V : Type u_2} [MeasurableSpace α] (μ : MeasureTheory.Measure α) [NormedAddCommGroup V] [InnerProductSpace ℝ V] (S : Set α) (hS : MeasurableSet S) (u : ↥(MeasureTheory.Lp V 2 μ)) : u ∈ supportedSpace μ S hS ↔ ∀ᵐ (x : α) ∂μ, x ∉ S → ↑↑u x = 0

Membership is exactly almost-everywhere vanishing outside the given set.

theorem EulerLpSupportedSubspace.supportedSpace_closed {α : Type u_1} {V : Type u_2} [MeasurableSpace α] (μ : MeasureTheory.Measure α) [NormedAddCommGroup V] [InnerProductSpace ℝ V] (S : Set α) (hS : MeasurableSet S) : IsClosed ↑(supportedSpace μ S hS)

The support condition is closed in the actual L² norm.

instance EulerLpSupportedSubspace.instCompleteSpaceSubtypeAEEqFunMemAddSubgroupLpOfNatENNRealSubmoduleRealSupportedSpace {α : Type u_1} {V : Type u_2} [MeasurableSpace α] (μ : MeasureTheory.Measure α) [NormedAddCommGroup V] [InnerProductSpace ℝ V] (S : Set α) (hS : MeasurableSet S) [CompleteSpace V] : CompleteSpace ↥(supportedSpace μ S hS)

@[reducible]

noncomputable instance EulerLpSupportedSubspace.supportedSpace.instSub {α : Type u_1} {V : Type u_2} [MeasurableSpace α] (μ : MeasureTheory.Measure α) [NormedAddCommGroup V] [InnerProductSpace ℝ V] (S : Set α) (hS : MeasurableSet S) : Sub ↥(supportedSpace μ S hS)

Equations

• EulerLpSupportedSubspace.supportedSpace.instSub μ S hS = inferInstance

instance EulerLpSupportedSubspace.supportedSpace.instIsBoundedSMul {α : Type u_1} {V : Type u_2} [MeasurableSpace α] (μ : MeasureTheory.Measure α) [NormedAddCommGroup V] [InnerProductSpace ℝ V] (S : Set α) (hS : MeasurableSet S) : IsBoundedSMul ℝ ↥(supportedSpace μ S hS)

instance EulerLpSupportedSubspace.supportedSpace.instContinuousNeg {α : Type u_1} {V : Type u_2} [MeasurableSpace α] (μ : MeasureTheory.Measure α) [NormedAddCommGroup V] [InnerProductSpace ℝ V] (S : Set α) (hS : MeasurableSet S) : ContinuousNeg ↥(supportedSpace μ S hS)

@[reducible]

noncomputable instance EulerLpSupportedSubspace.supportedSpace.instAdd {α : Type u_1} {V : Type u_2} [MeasurableSpace α] (μ : MeasureTheory.Measure α) [NormedAddCommGroup V] [InnerProductSpace ℝ V] (S : Set α) (hS : MeasurableSet S) : Add ↥(supportedSpace μ S hS)

Equations

• EulerLpSupportedSubspace.supportedSpace.instAdd μ S hS = inferInstance

@[reducible]

noncomputable instance EulerLpSupportedSubspace.supportedSpace.instAddMonoid {α : Type u_1} {V : Type u_2} [MeasurableSpace α] (μ : MeasureTheory.Measure α) [NormedAddCommGroup V] [InnerProductSpace ℝ V] (S : Set α) (hS : MeasurableSet S) : AddMonoid ↥(supportedSpace μ S hS)

Equations

• EulerLpSupportedSubspace.supportedSpace.instAddMonoid μ S hS = inferInstance

@[reducible]

noncomputable instance EulerLpSupportedSubspace.supportedSpace.instSubNegMonoid {α : Type u_1} {V : Type u_2} [MeasurableSpace α] (μ : MeasureTheory.Measure α) [NormedAddCommGroup V] [InnerProductSpace ℝ V] (S : Set α) (hS : MeasurableSet S) : SubNegMonoid ↥(supportedSpace μ S hS)

Equations

• EulerLpSupportedSubspace.supportedSpace.instSubNegMonoid μ S hS = inferInstance

@[reducible]

noncomputable instance EulerLpSupportedSubspace.supportedSpace.instTopologicalSpace {α : Type u_1} {V : Type u_2} [MeasurableSpace α] (μ : MeasureTheory.Measure α) [NormedAddCommGroup V] [InnerProductSpace ℝ V] (S : Set α) (hS : MeasurableSet S) : TopologicalSpace ↥(supportedSpace μ S hS)

Equations

• EulerLpSupportedSubspace.supportedSpace.instTopologicalSpace μ S hS = inferInstance

@[reducible]

noncomputable instance EulerLpSupportedSubspace.supportedSpace.instZero {α : Type u_1} {V : Type u_2} [MeasurableSpace α] (μ : MeasureTheory.Measure α) [NormedAddCommGroup V] [InnerProductSpace ℝ V] (S : Set α) (hS : MeasurableSet S) : Zero ↥(supportedSpace μ S hS)

Equations

• EulerLpSupportedSubspace.supportedSpace.instZero μ S hS = inferInstance

@[reducible]

noncomputable instance EulerLpSupportedSubspace.supportedSpace.instUniformSpace {α : Type u_1} {V : Type u_2} [MeasurableSpace α] (μ : MeasureTheory.Measure α) [NormedAddCommGroup V] [InnerProductSpace ℝ V] (S : Set α) (hS : MeasurableSet S) : UniformSpace ↥(supportedSpace μ S hS)

Equations

• EulerLpSupportedSubspace.supportedSpace.instUniformSpace μ S hS = inferInstance

@[reducible]

noncomputable instance EulerLpSupportedSubspace.supportedSpace.instNeg {α : Type u_1} {V : Type u_2} [MeasurableSpace α] (μ : MeasureTheory.Measure α) [NormedAddCommGroup V] [InnerProductSpace ℝ V] (S : Set α) (hS : MeasurableSet S) : Neg ↥(supportedSpace μ S hS)

Equations

• EulerLpSupportedSubspace.supportedSpace.instNeg μ S hS = inferInstance

instance EulerLpSupportedSubspace.supportedSpace.instNormSMulClass {α : Type u_1} {V : Type u_2} [MeasurableSpace α] (μ : MeasureTheory.Measure α) [NormedAddCommGroup V] [InnerProductSpace ℝ V] (S : Set α) (hS : MeasurableSet S) : NormSMulClass ℝ ↥(supportedSpace μ S hS)

@[reducible]

noncomputable instance EulerLpSupportedSubspace.supportedSpace.instAddCommMonoid {α : Type u_1} {V : Type u_2} [MeasurableSpace α] (μ : MeasureTheory.Measure α) [NormedAddCommGroup V] [InnerProductSpace ℝ V] (S : Set α) (hS : MeasurableSet S) : AddCommMonoid ↥(supportedSpace μ S hS)

Equations

• EulerLpSupportedSubspace.supportedSpace.instAddCommMonoid μ S hS = inferInstance

@[reducible]

noncomputable instance EulerLpSupportedSubspace.supportedSpace.instDistribMulAction {α : Type u_1} {V : Type u_2} [MeasurableSpace α] (μ : MeasureTheory.Measure α) [NormedAddCommGroup V] [InnerProductSpace ℝ V] (S : Set α) (hS : MeasurableSet S) : DistribMulAction ℝ ↥(supportedSpace μ S hS)

Equations

• EulerLpSupportedSubspace.supportedSpace.instDistribMulAction μ S hS = inferInstance

@[reducible]

noncomputable instance EulerLpSupportedSubspace.supportedSpace.instAddGroup {α : Type u_1} {V : Type u_2} [MeasurableSpace α] (μ : MeasureTheory.Measure α) [NormedAddCommGroup V] [InnerProductSpace ℝ V] (S : Set α) (hS : MeasurableSet S) : AddGroup ↥(supportedSpace μ S hS)

Equations

• EulerLpSupportedSubspace.supportedSpace.instAddGroup μ S hS = inferInstance

@[reducible]

noncomputable instance EulerLpSupportedSubspace.supportedSpace.instMulAction {α : Type u_1} {V : Type u_2} [MeasurableSpace α] (μ : MeasureTheory.Measure α) [NormedAddCommGroup V] [InnerProductSpace ℝ V] (S : Set α) (hS : MeasurableSet S) : MulAction ℝ ↥(supportedSpace μ S hS)

Equations

• EulerLpSupportedSubspace.supportedSpace.instMulAction μ S hS = inferInstance

@[reducible]

noncomputable instance EulerLpSupportedSubspace.supportedSpace.instNormedSpace {α : Type u_1} {V : Type u_2} [MeasurableSpace α] (μ : MeasureTheory.Measure α) [NormedAddCommGroup V] [InnerProductSpace ℝ V] (S : Set α) (hS : MeasurableSet S) : NormedSpace ℝ ↥(supportedSpace μ S hS)

Equations

• EulerLpSupportedSubspace.supportedSpace.instNormedSpace μ S hS = inferInstance

@[reducible]

noncomputable instance EulerLpSupportedSubspace.supportedSpace.instModule {α : Type u_1} {V : Type u_2} [MeasurableSpace α] (μ : MeasureTheory.Measure α) [NormedAddCommGroup V] [InnerProductSpace ℝ V] (S : Set α) (hS : MeasurableSet S) : Module ℝ ↥(supportedSpace μ S hS)

Equations

• EulerLpSupportedSubspace.supportedSpace.instModule μ S hS = inferInstance

@[reducible]

noncomputable instance EulerLpSupportedSubspace.supportedSpace.instMulActionWithZero {α : Type u_1} {V : Type u_2} [MeasurableSpace α] (μ : MeasureTheory.Measure α) [NormedAddCommGroup V] [InnerProductSpace ℝ V] (S : Set α) (hS : MeasurableSet S) : MulActionWithZero ℝ ↥(supportedSpace μ S hS)

Equations

• EulerLpSupportedSubspace.supportedSpace.instMulActionWithZero μ S hS = inferInstance

instance EulerLpSupportedSubspace.supportedSpace.instContinuousConstSMul {α : Type u_1} {V : Type u_2} [MeasurableSpace α] (μ : MeasureTheory.Measure α) [NormedAddCommGroup V] [InnerProductSpace ℝ V] (S : Set α) (hS : MeasurableSet S) : ContinuousConstSMul ℝ ↥(supportedSpace μ S hS)

@[reducible]

noncomputable instance EulerLpSupportedSubspace.supportedSpace.instAddCommGroup {α : Type u_1} {V : Type u_2} [MeasurableSpace α] (μ : MeasureTheory.Measure α) [NormedAddCommGroup V] [InnerProductSpace ℝ V] (S : Set α) (hS : MeasurableSet S) : AddCommGroup ↥(supportedSpace μ S hS)

Equations

• EulerLpSupportedSubspace.supportedSpace.instAddCommGroup μ S hS = inferInstance

instance EulerLpSupportedSubspace.supportedSpace.instIsUniformAddGroup {α : Type u_1} {V : Type u_2} [MeasurableSpace α] (μ : MeasureTheory.Measure α) [NormedAddCommGroup V] [InnerProductSpace ℝ V] (S : Set α) (hS : MeasurableSet S) : IsUniformAddGroup ↥(supportedSpace μ S hS)

instance EulerLpSupportedSubspace.supportedSpace.instIsTopologicalAddGroup {α : Type u_1} {V : Type u_2} [MeasurableSpace α] (μ : MeasureTheory.Measure α) [NormedAddCommGroup V] [InnerProductSpace ℝ V] (S : Set α) (hS : MeasurableSet S) : IsTopologicalAddGroup ↥(supportedSpace μ S hS)

@[reducible]

noncomputable instance EulerLpSupportedSubspace.supportedSpace.instNorm {α : Type u_1} {V : Type u_2} [MeasurableSpace α] (μ : MeasureTheory.Measure α) [NormedAddCommGroup V] [InnerProductSpace ℝ V] (S : Set α) (hS : MeasurableSet S) : Norm ↥(supportedSpace μ S hS)

Equations

• EulerLpSupportedSubspace.supportedSpace.instNorm μ S hS = inferInstance

@[reducible]

noncomputable instance EulerLpSupportedSubspace.supportedSpace.instNormedAddCommGroup {α : Type u_1} {V : Type u_2} [MeasurableSpace α] (μ : MeasureTheory.Measure α) [NormedAddCommGroup V] [InnerProductSpace ℝ V] (S : Set α) (hS : MeasurableSet S) : NormedAddCommGroup ↥(supportedSpace μ S hS)

Equations

• EulerLpSupportedSubspace.supportedSpace.instNormedAddCommGroup μ S hS = inferInstance

@[reducible]

noncomputable instance EulerLpSupportedSubspace.supportedSpace.instSeminormedAddGroup {α : Type u_1} {V : Type u_2} [MeasurableSpace α] (μ : MeasureTheory.Measure α) [NormedAddCommGroup V] [InnerProductSpace ℝ V] (S : Set α) (hS : MeasurableSet S) : SeminormedAddGroup ↥(supportedSpace μ S hS)

Equations

• EulerLpSupportedSubspace.supportedSpace.instSeminormedAddGroup μ S hS = inferInstance

@[reducible]

noncomputable instance EulerLpSupportedSubspace.supportedSpace.instDistribSMul {α : Type u_1} {V : Type u_2} [MeasurableSpace α] (μ : MeasureTheory.Measure α) [NormedAddCommGroup V] [InnerProductSpace ℝ V] (S : Set α) (hS : MeasurableSet S) : DistribSMul ℝ ↥(supportedSpace μ S hS)

Equations

• EulerLpSupportedSubspace.supportedSpace.instDistribSMul μ S hS = inferInstance

@[reducible]

noncomputable instance EulerLpSupportedSubspace.supportedSpace.instSMulWithZero {α : Type u_1} {V : Type u_2} [MeasurableSpace α] (μ : MeasureTheory.Measure α) [NormedAddCommGroup V] [InnerProductSpace ℝ V] (S : Set α) (hS : MeasurableSet S) : SMulWithZero ℝ ↥(supportedSpace μ S hS)

Equations

• EulerLpSupportedSubspace.supportedSpace.instSMulWithZero μ S hS = inferInstance

instance EulerLpSupportedSubspace.supportedSpace.instContinuousAdd {α : Type u_1} {V : Type u_2} [MeasurableSpace α] (μ : MeasureTheory.Measure α) [NormedAddCommGroup V] [InnerProductSpace ℝ V] (S : Set α) (hS : MeasurableSet S) : ContinuousAdd ↥(supportedSpace μ S hS)

@[reducible]

noncomputable instance EulerLpSupportedSubspace.supportedSpace.instPseudoMetricSpace {α : Type u_1} {V : Type u_2} [MeasurableSpace α] (μ : MeasureTheory.Measure α) [NormedAddCommGroup V] [InnerProductSpace ℝ V] (S : Set α) (hS : MeasurableSet S) : PseudoMetricSpace ↥(supportedSpace μ S hS)

Equations

• EulerLpSupportedSubspace.supportedSpace.instPseudoMetricSpace μ S hS = inferInstance

@[reducible]

noncomputable instance EulerLpSupportedSubspace.supportedSpace.instSMul {α : Type u_1} {V : Type u_2} [MeasurableSpace α] (μ : MeasureTheory.Measure α) [NormedAddCommGroup V] [InnerProductSpace ℝ V] (S : Set α) (hS : MeasurableSet S) : SMul ℝ ↥(supportedSpace μ S hS)

Equations

• EulerLpSupportedSubspace.supportedSpace.instSMul μ S hS = inferInstance

@[reducible]

noncomputable instance EulerLpSupportedSubspace.supportedSpace.instSeminormedAddCommGroup {α : Type u_1} {V : Type u_2} [MeasurableSpace α] (μ : MeasureTheory.Measure α) [NormedAddCommGroup V] [InnerProductSpace ℝ V] (S : Set α) (hS : MeasurableSet S) : SeminormedAddCommGroup ↥(supportedSpace μ S hS)

Equations

• EulerLpSupportedSubspace.supportedSpace.instSeminormedAddCommGroup μ S hS = NormedAddCommGroup.toSeminormedAddCommGroup

@[reducible]

noncomputable instance EulerLpSupportedSubspace.supportedSpace.instMetricSpace {α : Type u_1} {V : Type u_2} [MeasurableSpace α] (μ : MeasureTheory.Measure α) [NormedAddCommGroup V] [InnerProductSpace ℝ V] (S : Set α) (hS : MeasurableSet S) : MetricSpace ↥(supportedSpace μ S hS)

Equations

• EulerLpSupportedSubspace.supportedSpace.instMetricSpace μ S hS = inferInstance

@[reducible]

noncomputable instance EulerLpSupportedSubspace.supportedSpace.instNormedAddGroup {α : Type u_1} {V : Type u_2} [MeasurableSpace α] (μ : MeasureTheory.Measure α) [NormedAddCommGroup V] [InnerProductSpace ℝ V] (S : Set α) (hS : MeasurableSet S) : NormedAddGroup ↥(supportedSpace μ S hS)

Equations

• EulerLpSupportedSubspace.supportedSpace.instNormedAddGroup μ S hS = inferInstance

@[reducible]

noncomputable instance EulerLpSupportedSubspace.supportedSpace.instAddZeroClass {α : Type u_1} {V : Type u_2} [MeasurableSpace α] (μ : MeasureTheory.Measure α) [NormedAddCommGroup V] [InnerProductSpace ℝ V] (S : Set α) (hS : MeasurableSet S) : AddZeroClass ↥(supportedSpace μ S hS)

Equations

• EulerLpSupportedSubspace.supportedSpace.instAddZeroClass μ S hS = inferInstance

instance EulerLpSupportedSubspace.supportedSpace.instContinuousSub {α : Type u_1} {V : Type u_2} [MeasurableSpace α] (μ : MeasureTheory.Measure α) [NormedAddCommGroup V] [InnerProductSpace ℝ V] (S : Set α) (hS : MeasurableSet S) : ContinuousSub ↥(supportedSpace μ S hS)

instance EulerLpSupportedSubspace.supportedSpace.instContinuousSMul {α : Type u_1} {V : Type u_2} [MeasurableSpace α] (μ : MeasureTheory.Measure α) [NormedAddCommGroup V] [InnerProductSpace ℝ V] (S : Set α) (hS : MeasurableSet S) : ContinuousSMul ℝ ↥(supportedSpace μ S hS)

@[reducible]

noncomputable instance EulerLpSupportedSubspace.supportedSpace.instSMulZeroClass {α : Type u_1} {V : Type u_2} [MeasurableSpace α] (μ : MeasureTheory.Measure α) [NormedAddCommGroup V] [InnerProductSpace ℝ V] (S : Set α) (hS : MeasurableSet S) : SMulZeroClass ℝ ↥(supportedSpace μ S hS)

Equations

• EulerLpSupportedSubspace.supportedSpace.instSMulZeroClass μ S hS = inferInstance

theorem EulerLpSupportedSubspace.cutoff_mem {α : Type u_1} {V : Type u_2} [MeasurableSpace α] (μ : MeasureTheory.Measure α) [NormedAddCommGroup V] [InnerProductSpace ℝ V] (S : Set α) (hS : MeasurableSet S) (u : ↥(MeasureTheory.Lp V 2 μ)) : cutoff μ S hS u ∈ supportedSpace μ S hS

Every cutoff output belongs to the supported subspace.

noncomputable def EulerLpSupportedSubspace.projection {α : Type u_1} {V : Type u_2} [MeasurableSpace α] (μ : MeasureTheory.Measure α) [NormedAddCommGroup V] [InnerProductSpace ℝ V] (S : Set α) (hS : MeasurableSet S) : ↥(MeasureTheory.Lp V 2 μ) →L[ℝ] ↥(supportedSpace μ S hS)

Actual projection from full spatial L² to its supported Hilbert subspace.

Equations

• EulerLpSupportedSubspace.projection μ S hS = (EulerLpSupportedSubspace.cutoffOperator μ S hS).codRestrict (EulerLpSupportedSubspace.supportedSpace μ S hS) ⋯

theorem EulerLpSupportedSubspace.projection_norm {α : Type u_1} {V : Type u_2} [MeasurableSpace α] (μ : MeasureTheory.Measure α) [NormedAddCommGroup V] [InnerProductSpace ℝ V] (S : Set α) (hS : MeasurableSet S) : ‖projection μ S hS‖ ≤ 1

The projection has norm at most one.

theorem EulerLpSupportedSubspace.projection_supported {α : Type u_1} {V : Type u_2} [MeasurableSpace α] (μ : MeasureTheory.Measure α) [NormedAddCommGroup V] [InnerProductSpace ℝ V] (S : Set α) (hS : MeasurableSet S) (u : ↥(supportedSpace μ S hS)) : (projection μ S hS) ↑u = u

Inclusion after projection fixes every already supported field.