comp — Mathlib

English

Let g be strictly monotone on t and f be strictly anti on s. Then g ∘ f is strictly anti on s.

Русский

Пусть g строго монотонна на t, f строго антитонична на s. Тогда g ∘ f строго антитонична на s.

LaTeX

$$$(\forall x\in t)(\forall y\in t)(xf(y)) \Rightarrow \forall x,y\in s( xg(f(y)) ).$$$

Lean4

theorem comp (hg : StrictAntiOn g t) (hf : StrictAntiOn f s) (hs : Set.MapsTo f s t) : StrictMonoOn (g ∘ f) s :=
  fun _x hx _y hy hxy ↦ hg (hs hy) (hs hx) <| hf hx hy hxy

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