English
If f1 ≤ f2 and g1 ≤ᶠ[f1] g2, then bind f1 g1 ≤ bind f2 g2. A monotonicity property of bind in both arguments.
Русский
Если f1 ≤ f2 и g1 ≤ᶠ[f1] g2, то bind f1 g1 ≤ bind f2 g2. Свойство монотонности привязки по обеим аргументам.
LaTeX
$$$f_1 \\leq f_2 \\;\\land\\; g_1 \\leq^\\!_{f_1} g_2 \\Rightarrow f_1.\\mathrm{bind}\\ g_1 \\leq f_2.\\mathrm{bind}\\ g_2$$$
Lean4
@[mono]
theorem bind_mono {f₁ f₂ : Filter α} {g₁ g₂ : α → Filter β} (hf : f₁ ≤ f₂) (hg : g₁ ≤ᶠ[f₁] g₂) :
bind f₁ g₁ ≤ bind f₂ g₂ :=
by
refine le_trans (fun s hs => ?_) (join_mono <| map_mono hf)
simp only [mem_join, mem_bind', mem_map] at hs ⊢
filter_upwards [hg, hs] with _ hx hs using hx hs
