α : Type u_1
β : Type ?u.42082
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure (Measure (Measure α))
⊢ bind μ join = join (join μ)
α : Type u_1
β : Type ?u.42082
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure (Measure (Measure α))
⊢ join (map join μ) = join (join μ)
show bind μ join = join (join μ)
α : Type u_1
β : Type ?u.42082
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure (Measure (Measure α))
⊢ bind μ join = bind μ fun a => bind (id a) id
α : Type u_1
β : Type ?u.42082
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure (Measure (Measure α))
⊢ bind μ join = join (join μ)
rw [join_eq_bind, join_eq_bind, bind_bind measurable_id measurable_id]
α : Type u_1
β : Type ?u.42082
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure (Measure (Measure α))
⊢ join = fun a => bind (id a) id
α : Type u_1
β : Type ?u.42082
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure (Measure (Measure α))
⊢ bind μ join = bind μ fun a => bind (id a) id
apply congr_arg (bind μ)
case h
α : Type u_1
β : Type ?u.42082
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure (Measure (Measure α))
ν : Measure (Measure α)
⊢ join ν = bind (id ν) id
α : Type u_1
β : Type ?u.42082
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure (Measure (Measure α))
⊢ join = fun a => bind (id a) id
funext ν
no goals
case h
α : Type u_1
β : Type ?u.42082
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure (Measure (Measure α))
ν : Measure (Measure α)
⊢ join ν = bind (id ν) id
exact join_eq_bind ν