compRel — Mathlib

English

If f and g are monotone as functions to sets of pairs, then x ↦ f(x) ∘ g(x) is monotone.

Русский

Если f и g монотонны как функции, принимающие множества пар, то x ↦ f(x) ∘ g(x) монотонно по x.

LaTeX

$$$\operatorname{Monotone}(x \mapsto f(x) \circ g(x))$$$

Lean4

theorem compRel [Preorder β] {f g : β → Set (α × α)} (hf : Monotone f) (hg : Monotone g) :
    Monotone fun x => f x ○ g x := fun _ _ h _ ⟨z, h₁, h₂⟩ => ⟨z, hf h h₁, hg h h₂⟩

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