theorem
modification_of_indistinguishable
{T : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{X Y : T → Ω → E}
(h : ∀ᵐ (ω : Ω) ∂P, ∀ (t : T), X t ω = Y t ω)
(t : T)
:
theorem
indistinguishable_of_modification
{T : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{X Y : T → Ω → E}
[TopologicalSpace E]
[TopologicalSpace T]
[TopologicalSpace.SeparableSpace T]
[T2Space E]
(hX : ∀ᵐ (ω : Ω) ∂P, Continuous fun (t : T) => X t ω)
(hY : ∀ᵐ (ω : Ω) ∂P, Continuous fun (t : T) => Y t ω)
(h : ∀ (t : T), X t =ᵐ[P] Y t)
:
theorem
subset_closure_dense_inter
{α : Type u_4}
[TopologicalSpace α]
{T' U : Set α}
(hT'_dense : Dense T')
(hU : IsOpen U)
:
theorem
indistinguishable_of_modification_on
{T : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{X Y : T → Ω → E}
[TopologicalSpace E]
[TopologicalSpace T]
[TopologicalSpace.SeparableSpace T]
[T2Space E]
{U : Set T}
(hU : IsOpen U)
(hX : ∀ᵐ (ω : Ω) ∂P, ContinuousOn (fun (x : T) => X x ω) U)
(hY : ∀ᵐ (ω : Ω) ∂P, ContinuousOn (fun (x : T) => Y x ω) U)
(h : ∀ t ∈ U, X t =ᵐ[P] Y t)
: