univLE_of_injective — Mathlib

English

If there exists an injective function f from Ordinal_u to Ordinal_v, then UnivLE(u,v) holds.

Русский

Если существует инъективная функция f: Ordinal_u → Ordinal_v, то UnivLE(u,v) выполняется.

LaTeX

$$$ \\forall f:\\mathrm{Ord}_u \\to \\mathrm{Ord}_v,\\; f \\text{ injective} \\Rightarrow UnivLE(u,v) $$$

Lean4

theorem univLE_of_injective {f : Ordinal.{u} → Ordinal.{v}} (h : f.Injective) : UnivLE.{u, v} :=
  univLE_iff_exists_embedding.2 ⟨f, h⟩

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