α : Type u_1
β : Type ?u.224536
γ : Type ?u.224539
ι : Type ?u.224542
inst✝² : Countable ι
f✝ g✝ : α → β
m : MeasurableSpace α
E : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : MetrizableSpace E
f g : α → E
hf : StronglyMeasurable f
hg : StronglyMeasurable g
this✝¹ : MeasurableSpace (E × E) := borel (E × E)
this✝ : BorelSpace (E × E)
⊢ MeasurableSet {x | f x = g x}
α : Type u_1
β : Type ?u.224536
γ : Type ?u.224539
ι : Type ?u.224542
inst✝² : Countable ι
f✝ g✝ : α → β
m : MeasurableSpace α
E : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : MetrizableSpace E
f g : α → E
hf : StronglyMeasurable f
hg : StronglyMeasurable g
⊢ MeasurableSet {x | f x = g x}
borelize (E × E)
no goals
α : Type u_1
β : Type ?u.224536
γ : Type ?u.224539
ι : Type ?u.224542
inst✝² : Countable ι
f✝ g✝ : α → β
m : MeasurableSpace α
E : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : MetrizableSpace E
f g : α → E
hf : StronglyMeasurable f
hg : StronglyMeasurable g
this✝¹ : MeasurableSpace (E × E) := borel (E × E)
this✝ : BorelSpace (E × E)
⊢ MeasurableSet {x | f x = g x}
exact (hf.prod_mk hg).measurable isClosed_diagonal.measurableSet