comp_antitoneOn_right — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem comp_antitoneOn_right (h : MonovaryOn f g s) (hg : AntitoneOn g' (g '' s)) : AntivaryOn f (g' ∘ g) s :=
  fun _ hi _ hj hij => h hj hi <| hg.reflect_lt (mem_image_of_mem _ hi) (mem_image_of_mem _ hj) hij

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