comp_strictAntiOn — Mathlib

English

Let g be strictly antitone on t and f be strictly antitone on s. Then g ∘ f is strictly monotone on s given MapsTo f s t.

Русский

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

LaTeX

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

Lean4

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

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