α : Type u
β : Type v
γ : Type w
δ : Type ?u.298298
ι : Sort x
f₁ f₂ : Filter α
g₁ g₂ : α → Filter β
hf : f₁ ≤ f₂
hg : g₁ ≤ᶠ[f₁] g₂
s : Set β
hs : s ∈ join (map g₂ f₁)
⊢ s ∈ bind f₁ g₁
α : Type u
β : Type v
γ : Type w
δ : Type ?u.298298
ι : Sort x
f₁ f₂ : Filter α
g₁ g₂ : α → Filter β
hf : f₁ ≤ f₂
hg : g₁ ≤ᶠ[f₁] g₂
⊢ bind f₁ g₁ ≤ bind f₂ g₂
refine' le_trans (fun s hs => _) (join_mono <| map_mono hf)
α : Type u
β : Type v
γ : Type w
δ : Type ?u.298298
ι : Sort x
f₁ f₂ : Filter α
g₁ g₂ : α → Filter β
hf : f₁ ≤ f₂
hg : g₁ ≤ᶠ[f₁] g₂
s : Set β
hs : g₂ ⁻¹' {t | s ∈ t} ∈ f₁
⊢ {a | s ∈ g₁ a} ∈ f₁
α : Type u
β : Type v
γ : Type w
δ : Type ?u.298298
ι : Sort x
f₁ f₂ : Filter α
g₁ g₂ : α → Filter β
hf : f₁ ≤ f₂
hg : g₁ ≤ᶠ[f₁] g₂
s : Set β
hs : s ∈ join (map g₂ f₁)
⊢ s ∈ bind f₁ g₁
simp only [mem_join, mem_bind', mem_map] at hs ⊢
no goals
α : Type u
β : Type v
γ : Type w
δ : Type ?u.298298
ι : Sort x
f₁ f₂ : Filter α
g₁ g₂ : α → Filter β
hf : f₁ ≤ f₂
hg : g₁ ≤ᶠ[f₁] g₂
s : Set β
hs : g₂ ⁻¹' {t | s ∈ t} ∈ f₁
⊢ {a | s ∈ g₁ a} ∈ f₁
filter_upwards [hg, hs] with _ hx hs using hx hs