ofEssSurj — Mathlib

English

If there exists an ess-surjection w for uliftFunctor, then UnivLE holds (constructed from w).

Русский

Если существует ess-покрытие w для uliftFunctor, тогда выполняется UnivLE, сконструированная из w.

LaTeX

$$$ w:\\, (\\mathrm{uliftFunctor}_{u,v} : \\mathrm{Type}\\,v \\to \\mathrm{Type}\\,\\max u\,v).\\mathrm{EssSurj} \\Rightarrow \\mathrm{UnivLE}^{\\max u\,v,\\,v}. $$$

Lean4

theorem ofEssSurj (w : (uliftFunctor.{u, v} : Type v ⥤ Type max u v).EssSurj) : UnivLE.{max u v, v} where
  small
    α := by
    obtain ⟨a', ⟨m⟩⟩ := w.mem_essImage α
    exact ⟨a', ⟨(Iso.toEquiv m).symm.trans Equiv.ulift⟩⟩

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