lt_univ' — Mathlib

English

A cardinal c is less than the universe iff there exists c' with c = lift^{max(u+1,v),u}(c').

Русский

Кардинал c меньше вселенной тогда и только тогда, когда существует c' такой, что c = lift^{max(u+1,v),u}(c').

LaTeX

$$$c < \\mathrm{univ}^{u,v} \\iff \\exists c',\\ c = \\mathrm{lift}^{\\max(u+1,v),u}(c')$$$

Lean4

theorem lt_univ' {c} : c < univ.{u, v} ↔ ∃ c', c = lift.{max (u + 1) v, u} c' :=
  ⟨fun h => by
    let ⟨a, h', e⟩ := lt_lift_iff.1 h
    rw [← univ_id] at h'
    rcases lt_univ.{u}.1 h' with ⟨c', rfl⟩
    exact ⟨c', by simp only [e.symm, lift_lift]⟩, fun ⟨_, e⟩ => e.symm ▸ lift_lt_univ' _⟩

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