univLE_iff_exists_embedding — Mathlib

English

Two universes are related by UnivLE exactly when there exists an embedding from ordinals at the first level into ordinals at the second level.

Русский

Связь между двумя вселенными через UnivLE возникает тогда и только тогда, когда существует вложение из порядков первого уровня в порядки второго уровня.

LaTeX

$$$ UnivLE(u,v) \\iff \\exists f:\\mathrm{Ord}_u \\hookrightarrow \\mathrm{Ord}_v, \\; f \\text{ является вложением} $$$

Lean4

theorem univLE_iff_exists_embedding : UnivLE.{u, v} ↔ Nonempty (Ordinal.{u} ↪ Ordinal.{v}) :=
  by
  rw [univLE_iff_cardinal_le]
  exact lift_mk_le'

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