English
Let u and v be universe levels. Then UnivLE(u,v) holds if and only if the first universe, viewed in the second level, is at most the second universe viewed in the first level.
Русский
Пусть u и v — уровни вселенных. Тогда UnivLE(u,v) истинно тогда и только тогда, когда первая вселенная, восприятная во втором уровне, не превосходит вторую вселенную, воспринимаемую в первом уровне.
LaTeX
$$$ UnivLE(u,v) \\iff \\operatorname{univ}_{u,v+1} \\le \\operatorname{univ}_{v,u+1} $$$
Lean4
theorem univLE_iff_cardinal_le : 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_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_umax.{v, u}, ← lift_le.{u + 1}, lift_univ, lift_lift]
exact h.le
