comp_monotoneOn_right — Mathlib

English

If h is MonovaryOn f g on s and g' is MonotoneOn 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 MonotoneOn\\;g'\\;(g''s) \\Rightarrow MonovaryOn\\;f\\;(g'\\circ g)\\;s $$$$

Lean4

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

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