comp_strictMono — Mathlib

English

Let g be strictly antitone and f be strictly monotone. Then the composition g ∘ f is strictly antitone.

Русский

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

LaTeX

$$$\left( \forall x,y\in\beta,\ xg(y)\right) \wedge \left( \forall a,b\in\alpha,\ ag(f(b)).$$$

Lean4

theorem comp_strictMono (hg : StrictAnti g) (hf : StrictMono f) : StrictAnti (g ∘ f) := fun _ _ h ↦ hg (hf h)

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