α : Type u_1
β : Type u_2
ι : Type ?u.1453265
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
γ : Type u_3
mγ : MeasurableSpace γ
f : γ → β
κ : { x // x ∈ kernel α β }
hf : MeasurableEmbedding f
hκ : ∀ (a : α), ↑↑(↑κ a) (Set.range f) = 1
a : α
⊢ ↑↑(↑(kernel.comapRight κ hf) a) Set.univ = 1
α : Type u_1
β : Type u_2
ι : Type ?u.1453265
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
γ : Type u_3
mγ : MeasurableSpace γ
f : γ → β
κ : { x // x ∈ kernel α β }
hf : MeasurableEmbedding f
hκ : ∀ (a : α), ↑↑(↑κ a) (Set.range f) = 1
⊢ IsMarkovKernel (kernel.comapRight κ hf)
refine' ⟨fun a => ⟨_⟩⟩
α : Type u_1
β : Type u_2
ι : Type ?u.1453265
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
γ : Type u_3
mγ : MeasurableSpace γ
f : γ → β
κ : { x // x ∈ kernel α β }
hf : MeasurableEmbedding f
hκ : ∀ (a : α), ↑↑(↑κ a) (Set.range f) = 1
a : α
⊢ ↑↑(↑κ a) (f '' Set.univ) = 1
α : Type u_1
β : Type u_2
ι : Type ?u.1453265
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
γ : Type u_3
mγ : MeasurableSpace γ
f : γ → β
κ : { x // x ∈ kernel α β }
hf : MeasurableEmbedding f
hκ : ∀ (a : α), ↑↑(↑κ a) (Set.range f) = 1
a : α
⊢ ↑↑(↑(kernel.comapRight κ hf) a) Set.univ = 1
rw [comapRight_apply' κ hf a MeasurableSet.univ]
α : Type u_1
β : Type u_2
ι : Type ?u.1453265
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
γ : Type u_3
mγ : MeasurableSpace γ
f : γ → β
κ : { x // x ∈ kernel α β }
hf : MeasurableEmbedding f
hκ : ∀ (a : α), ↑↑(↑κ a) (Set.range f) = 1
a : α
⊢ ↑↑(↑κ a) (Set.range f) = 1
α : Type u_1
β : Type u_2
ι : Type ?u.1453265
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
γ : Type u_3
mγ : MeasurableSpace γ
f : γ → β
κ : { x // x ∈ kernel α β }
hf : MeasurableEmbedding f
hκ : ∀ (a : α), ↑↑(↑κ a) (Set.range f) = 1
a : α
⊢ ↑↑(↑κ a) (f '' Set.univ) = 1
simp only [Set.image_univ, Subtype.range_coe_subtype, Set.setOf_mem_eq]
no goals
α : Type u_1
β : Type u_2
ι : Type ?u.1453265
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
γ : Type u_3
mγ : MeasurableSpace γ
f : γ → β
κ : { x // x ∈ kernel α β }
hf : MeasurableEmbedding f
hκ : ∀ (a : α), ↑↑(↑κ a) (Set.range f) = 1
a : α
⊢ ↑↑(↑κ a) (Set.range f) = 1
exact hκ a