trans — Mathlib

English

The composition of two normal ordinal functions is normal: if f and g are normal, then f ∘ g is normal.

Русский

Сопоставление двух нормальных функций по ординалам нормализует результат: если f и g нормальны, то f ∘ g нормальна.

LaTeX

$$$\forall f\,\forall g\; (\mathrm{IsNormal}(f) \land \mathrm{IsNormal}(g)) \to \mathrm{IsNormal}(f \circ g).$$$

Lean4

theorem trans {f g} (H₁ : IsNormal f) (H₂ : IsNormal g) : IsNormal (f ∘ g) :=
  H₁.comp H₂

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