antivary — Mathlib

English

If h is MonovaryOn f g on s and g' is monotone on the image g(s), then f and g'∘g are MonovaryOn on s.

Русский

Если h = MonovaryOn f g на s, а g' монотонна на образе g(s), тогда MonovaryOn f (g'∘g) на s.

LaTeX

$$$$ MonovaryOn\\;f\\;g\\;s \\land MonotoneOn\\;g'\\;(g''s) \\Rightarrow MonovaryOn\\;f\\;(g'\\circ g)\\;s $$$$

Lean4

protected theorem antivary (hf : Antitone f) (hg : Monotone g) : Antivary f g :=
  (hf.monovary hg.dual_right).dual_right

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