case h
α : Type u_1
β : Type u_2
ι : Type ?u.1444502
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : { x // x ∈ kernel α β }
s t : Set β
a : α
⊢ ↑(kernel.restrict κ (_ : MeasurableSet Set.univ)) a = ↑κ a
α : Type u_1
β : Type u_2
ι : Type ?u.1444502
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : { x // x ∈ kernel α β }
s t : Set β
⊢ kernel.restrict κ (_ : MeasurableSet Set.univ) = κ
ext1 a
no goals
case h
α : Type u_1
β : Type u_2
ι : Type ?u.1444502
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : { x // x ∈ kernel α β }
s t : Set β
a : α
⊢ ↑(kernel.restrict κ (_ : MeasurableSet Set.univ)) a = ↑κ a
rw [kernel.restrict_apply, Measure.restrict_univ]