instOfNonempty — Mathlib

English

The axiom of choice implies that every nonempty type is an injective object in the category of types.

Русский

Аксиома выбора приводит к тому, что любой непустой тип является инъективным объектом в категории типов.

LaTeX

$$$$\text{Injective}(X) \quad\text{for any nonempty type } X.$$$$

Lean4

/-- The axiom of choice says that every nonempty type is an injective object in `Type`. -/
instance (X : Type u₁) [Nonempty X] : Injective X where
  factors g f
    mono :=
    ⟨fun z => by classical exact if h : z ∈ Set.range f then g (Classical.choose h) else Nonempty.some inferInstance,
      by
      ext y
      classical
      change dite (f y ∈ Set.range f) (fun h => g (Classical.choose h)) _ = _
      split_ifs <;> rename_i h
      · rw [mono_iff_injective] at mono
        rw [mono (Classical.choose_spec h)]
      · exact False.elim (h ⟨y, rfl⟩)⟩

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