comp — Mathlib

English

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

Русский

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

LaTeX

$$$\IsNormal(g \circ f)$$$

Lean4

theorem comp (hg : IsNormal g) (hf : IsNormal f) : IsNormal (g ∘ f) :=
  by
  refine ⟨hg.strictMono.comp hf.strictMono, fun ha b hb ↦ ?_⟩
  simp_rw [Function.comp_apply, mem_upperBounds, forall_mem_image] at hb
  simpa [hg.le_iff_forall_le (hf.map_isSuccLimit ha), hf.lt_iff_exists_lt ha] using fun c d hd hc ↦
    (hg.strictMono hc).le.trans (hb hd)

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