theorem
modification_of_indistinduishable
{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
indistinduishable_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)
: