comp_strictAntiOn — Mathlib

English

Let g be strictly antitone on t and f be strictly antitone on s, with f mapping s into t. Then g ∘ f is strictly monotone on s.

Русский

Пусть 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

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

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