relComp — Mathlib

English

The map x ↦ f(x) ○ g(x) is monotone if f and g are monotone in x.

Русский

Отображение x ↦ f(x) ○ g(x) монотонно, если f и g монотонны по x.

LaTeX

$$Monotone f \Rightarrow Monotone g \Rightarrow Monotone (\lambda x. f x \circ g x)$$

Lean4

protected theorem _root_.Monotone.relComp {ι : Type*} [Preorder ι] {f : ι → SetRel α β} {g : ι → SetRel β γ}
    (hf : Monotone f) (hg : Monotone g) : Monotone fun x ↦ f x ○ g x := fun _i _j hij ⟨_a, _c⟩ ⟨b, hab, hbc⟩ ↦
  ⟨b, hf hij hab, hg hij hbc⟩

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