partBind — Mathlib

English

If f and g are antitone, then x ↦ (f x).bind (g x) is antitone.

Русский

Если f и g антимонотонны, то x ↦ (f x).bind (g x) антимонотонна.

LaTeX

$$$$ \\text{Antitone } f \\to \\text{Antitone } g \\to \\text{Antitone }(x \\mapsto (f x).bind (g x)). $$$$

Lean4

theorem partBind (hf : Antitone f) (hg : Antitone g) : Antitone fun x ↦ (f x).bind (g x) :=
  by
  rintro x y h a
  simp only [and_imp, Part.mem_bind_iff, exists_imp]
  exact fun b hb ha ↦ ⟨b, hf h _ hb, hg h _ _ ha⟩

Похожие утверждения