comp_strictAntiOn — Mathlib

English

Let g be strictly monotone and f be strictly antitone on a set s. Then the composition g ∘ f is strictly monotone on s.

Русский

Пусть g строго монотонна, а f строго антитонична на s. Тогда композиция g ∘ f строго монотонна на s.

LaTeX

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

Lean4

theorem comp_strictAntiOn (hg : StrictMono g) (hf : StrictAntiOn f s) : StrictAntiOn (g ∘ f) s := fun _ ha _ hb h ↦
  hg (hf ha hb h)

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