not_small_type — Mathlib

English

There is no way to view all small types as a small type; Type max(u,v) is not small.

Русский

Нельзя представить множество всех малых типов как малый тип; Type(max(u,v)) не мал.

LaTeX

$$$\neg Small(\mathrm{Type}(\max(u,v))).$$$

Lean4

theorem not_small_type : ¬Small.{u} (Type max u v)
  | ⟨⟨S, ⟨e⟩⟩⟩ =>
    @Function.cantor_injective (Σ α, e.symm α) (fun a => ⟨_, cast (e.3 _).symm a⟩) fun a b e =>
      by
      dsimp at e
      injection e with h₁ h₂
      simpa using h₂

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