partSeq — Mathlib

English

If f: α → Part(β → γ) is antitone and g: α → Part β is antitone, then x ↦ f(x) <*> g(x) is antitone.

Русский

Пусть f: α → Part(β → γ) антимонотонна и g: α → Part β антимонотонна; тогда x ↦ f(x) <*> g(x) антимонотонно по x.

LaTeX

$$$\\mathrm{Antitone}(f) \\wedge \\mathrm{Antitone}(g) \\Rightarrow \\mathrm{Antitone}\\big( x \\mapsto f(x) \\\\; <*>\\\\ g(x) \\big)$$$

Lean4

theorem partSeq (hf : Antitone f) (hg : Antitone g) : Antitone fun x ↦ f x <*> g x := by
  simpa only [seq_eq_bind_map] using hf.partBind <| Antitone.of_apply₂ fun _ ↦ hg.partMap

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