Mathlib.SetTheory.Cardinal.UnivLE

univLE_iff_cardinal_le theorem

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

Full source

theorem univLE_iff_cardinal_le : UnivLEUnivLE.{u, v}UnivLE.{u, v} ↔ univ.{u, v+1} ≤ univ.{v, u+1} := by
  rw [← not_iff_not, univLE_iff]; simp_rw [small_iff_lift_mk_lt_univ]; push_neg
  -- strange: simp_rw [univ_umax.{v,u}] doesn't work
  refine ⟨fun ⟨α, le⟩ ↦ ?_, fun h ↦ ?_⟩
  · rw [univ_umaxuniv_umax.{v,u}, ← lift_le.{u+1}, lift_univ, lift_lift] at le
    exact le.trans_lt (lift_lt_univ'.{u,v+1} #α)
  · obtain ⟨⟨α⟩, h⟩ := lt_univ'.mp h; use α
    rw [univ_umaxuniv_umax.{v,u}, ← lift_le.{u+1}, lift_univ, lift_lift]
    exact h.le

Universe Level Inequality via Cardinal Comparison: $\text{UnivLE}(u, v) \leftrightarrow \#(\text{Type } u) \leq \#(\text{Type } v)$

Informal description

The universe level inequality `UnivLE.{u, v}` holds if and only if the cardinality of the universe `Type u` (lifted to universe `v + 1`) is less than or equal to the cardinality of the universe `Type v` (lifted to universe `u + 1`). That is, $\text{UnivLE}(u, v) \leftrightarrow \#(\text{Type } u) \leq \#(\text{Type } v)$, where the cardinalities are appropriately lifted to higher universes for comparison.

univLE_iff_exists_embedding theorem

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

Full source

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

Universe Level Inequality via Ordinal Embedding: $\text{UnivLE}(u, v) \leftrightarrow \text{Ordinal}_u \hookrightarrow \text{Ordinal}_v$

Informal description

The universe level inequality $\text{UnivLE}(u, v)$ holds if and only if there exists an injective function from the type of ordinals in universe $u$ to the type of ordinals in universe $v$. That is, $\text{UnivLE}(u, v) \leftrightarrow \exists f : \text{Ordinal}_u \hookrightarrow \text{Ordinal}_v$.

Ordinal.univLE_of_injective theorem

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

Full source

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

Universe Level Inequality via Ordinal Injection: $\text{Ordinal}_u \hookrightarrow \text{Ordinal}_v \Rightarrow \text{UnivLE}(u, v)$

Informal description

Given an injective function $f$ from the type of ordinals in universe $u$ to the type of ordinals in universe $v$, the universe level inequality $\text{UnivLE}(u, v)$ holds. That is, if there exists an injection $\text{Ordinal}_u \hookrightarrow \text{Ordinal}_v$, then every type in universe $u$ can be represented in universe $v$.

univLE_total theorem

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

Full source

/-- Together with transitivity, this shows `UnivLE` is a total preorder. -/
theorem univLE_total : UnivLEUnivLE.{u, v}UnivLE.{u, v} ∨ UnivLE.{v, u} := by
  simp_rw [univLE_iff_cardinal_le]; apply le_total

Total Preorder Property of Universe Level Inequality

Informal description

For any two universe levels $u$ and $v$, either every type in universe $u$ can be represented in universe $v$ (i.e., $\text{UnivLE}(u, v)$ holds), or every type in universe $v$ can be represented in universe $u$ (i.e., $\text{UnivLE}(v, u)$ holds).