comp — Mathlib

English

If g and f are RightOrdContinuous, then their composition g ∘ f is RightOrdContinuous.

Русский

Если g и f — правые непрерывности порядка, то композиция g ∘ f — правая непрерывность порядка.

LaTeX

$$$ \\text{RightOrdContinuous}(g) \\to \\text{RightOrdContinuous}(f) \\to \\text{RightOrdContinuous}(g \\circ f). $$$

Lean4

theorem comp (hg : RightOrdContinuous g) (hf : RightOrdContinuous f) : RightOrdContinuous (g ∘ f) :=
  hg.orderDual.comp hf.orderDual

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