instSubsingleton — Mathlib

English

The type F.FullyFaithful is a subsingleton, meaning any two instances of this structure are equal.

Русский

Тип F.FullyFaithful является субоднозначным: любые два экземпляра этой структуры равны.

LaTeX

$$$\text{Subsingleton } (F.FullyFaithful)$$$

Lean4

instance : Subsingleton F.FullyFaithful where
  allEq h₁
    h₂ := by
    have := h₁.faithful
    cases h₁ with
    | mk f₁ hf₁ _ =>
      cases h₂ with
      | mk f₂ hf₂ _ =>
        simp only [Functor.FullyFaithful.mk.injEq]
        ext
        apply F.map_injective
        rw [hf₁, hf₂]

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