α : Type u
α' : Type ?u.60176
β✝ : Type v
β' : Type ?u.60181
γ✝ : Type ?u.60184
φ : Type ?u.60187
inst✝⁵ : OmegaCompletePartialOrder α
inst✝⁴ : OmegaCompletePartialOrder β✝
inst✝³ : OmegaCompletePartialOrder γ✝
inst✝² : OmegaCompletePartialOrder φ
inst✝¹ : OmegaCompletePartialOrder α'
inst✝ : OmegaCompletePartialOrder β'
β γ : Type v
f : β → γ
g : α → Part β
hg : Continuous' g
⊢ Continuous' fun x => g x >>= pure ∘ f
α : Type u
α' : Type ?u.60176
β✝ : Type v
β' : Type ?u.60181
γ✝ : Type ?u.60184
φ : Type ?u.60187
inst✝⁵ : OmegaCompletePartialOrder α
inst✝⁴ : OmegaCompletePartialOrder β✝
inst✝³ : OmegaCompletePartialOrder γ✝
inst✝² : OmegaCompletePartialOrder φ
inst✝¹ : OmegaCompletePartialOrder α'
inst✝ : OmegaCompletePartialOrder β'
β γ : Type v
f : β → γ
g : α → Part β
hg : Continuous' g
⊢ Continuous' fun x => f <$> g x
simp only [map_eq_bind_pure_comp]
α : Type u
α' : Type ?u.60176
β✝ : Type v
β' : Type ?u.60181
γ✝ : Type ?u.60184
φ : Type ?u.60187
inst✝⁵ : OmegaCompletePartialOrder α
inst✝⁴ : OmegaCompletePartialOrder β✝
inst✝³ : OmegaCompletePartialOrder γ✝
inst✝² : OmegaCompletePartialOrder φ
inst✝¹ : OmegaCompletePartialOrder α'
inst✝ : OmegaCompletePartialOrder β'
β γ : Type v
f : β → γ
g : α → Part β
hg : Continuous' g
⊢ Continuous' fun x => pure ∘ f
α : Type u
α' : Type ?u.60176
β✝ : Type v
β' : Type ?u.60181
γ✝ : Type ?u.60184
φ : Type ?u.60187
inst✝⁵ : OmegaCompletePartialOrder α
inst✝⁴ : OmegaCompletePartialOrder β✝
inst✝³ : OmegaCompletePartialOrder γ✝
inst✝² : OmegaCompletePartialOrder φ
inst✝¹ : OmegaCompletePartialOrder α'
inst✝ : OmegaCompletePartialOrder β'
β γ : Type v
f : β → γ
g : α → Part β
hg : Continuous' g
⊢ Continuous' fun x => g x >>= pure ∘ f
apply bind_continuous' _ _ hg
no goals
α : Type u
α' : Type ?u.60176
β✝ : Type v
β' : Type ?u.60181
γ✝ : Type ?u.60184
φ : Type ?u.60187
inst✝⁵ : OmegaCompletePartialOrder α
inst✝⁴ : OmegaCompletePartialOrder β✝
inst✝³ : OmegaCompletePartialOrder γ✝
inst✝² : OmegaCompletePartialOrder φ
inst✝¹ : OmegaCompletePartialOrder α'
inst✝ : OmegaCompletePartialOrder β'
β γ : Type v
f : β → γ
g : α → Part β
hg : Continuous' g
⊢ Continuous' fun x => pure ∘ f
apply const_continuous'