comp — Mathlib

English

If g and f are left order continuous, then their composition g ∘ f is left order continuous.

Русский

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

LaTeX

$$$\text{LeftOrdContinuous}(g) \rightarrow \text{LeftOrdContinuous}(f) \rightarrow \text{LeftOrdContinuous}(\mathrm{Function.comp}\ g\ f)$$$

Lean4

theorem comp (hg : LeftOrdContinuous g) (hf : LeftOrdContinuous f) : LeftOrdContinuous (g ∘ f) := fun s x h => by
  simpa only [image_image] using hg (hf h)

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