equivEquivIso — Mathlib

English

Equivalences between finite types A ≃ B correspond to isomorphisms A ≅ B in the category FintypeCat.

Русский

Эквивалентности между конечными множества A ≃ B соответствуют изоморфизмам A ≅ B в FintypeCat.

LaTeX

$$$(A \\simeq B) \\;\\cong\\; (A \\cong B)$$$

Lean4

/-- Equivalences between finite types are the same as isomorphisms in `FintypeCat`. -/
@[simps]
def equivEquivIso {A B : FintypeCat} : A ≃ B ≃ (A ≅ B)
    where
  toFun
    e :=
    { hom := e
      inv := e.symm }
  invFun
    i :=
    { toFun := i.hom
      invFun := i.inv
      left_inv := congr_fun i.hom_inv_id
      right_inv := congr_fun i.inv_hom_id }
  left_inv := by cat_disch
  right_inv := by cat_disch

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