partMap — Mathlib

English

Let α, β, γ be types with a preorder on α. If g: α → Part β is antitone and f: β → γ, then the map x ↦ (g(x)).map f is antitone.

Русский

Пусть α, β, γ — множества с предельной упорядоченностью. Если g: α → Part β антимонотна и f: β → γ, то отображение x ↦ (g(x)).map f антимонотно по x.

LaTeX

$$$\\mathrm{Antitone}(g) \\Rightarrow \\mathrm{Antitone}\\big( x \\mapsto \\mathrm{Part.map}\\, f\\, (g\\,x) \\big)$$$

Lean4

theorem partMap (hg : Antitone g) : Antitone fun x ↦ (g x).map f := by
  simpa only [← bind_some_eq_map] using hg.partBind antitone_const

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