UnivLE and cardinals

theorem univLE_iff_cardinal_le : UnivLE.{u, v} ↔ Cardinal.univ.{u, v + 1} ≤ Cardinal.univ.{v, u + 1}

theorem univLE_iff_exists_embedding : UnivLE.{u, v} ↔ Nonempty (Ordinal.{u} ↪ Ordinal.{v})

theorem Ordinal.univLE_of_injective {f : Ordinal.{u} → Ordinal.{v}} (h : Function.Injective f) : UnivLE.{u, v}

theorem univLE_total : UnivLE.{u, v} ∨ UnivLE.{v, u}

Together with transitivity, this shows UnivLE is a total preorder.