comp — Mathlib

English

The composition of two bundled monotone maps is monotone and is itself an OrderHom.

Русский

Композиця двух упакованных монотонных отображений образует новый OrderHom.

LaTeX

$$$\\text{comp}(g,f) = g \\circ f$ as an OrderHom$$$

Lean4

/-- The composition of two bundled monotone functions. -/
@[simps -fullyApplied]
def comp (g : β →o γ) (f : α →o β) : α →o γ :=
  ⟨g ∘ f, g.mono.comp f.mono⟩

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