of_equivalence — Mathlib

English

If α: C ≌ D is an equivalence and C has a Coseparator, then D has a Coseparator.

Русский

Если C имеет косепаратор и существует эквивалентность между C и D, то D имеет косепаратор.

LaTeX

$$$\mathrm{HasCoseparator}(D)$$$

Lean4

theorem of_equivalence [HasCoseparator C] (α : C ≌ D) : HasCoseparator D :=
  ⟨α.functor.obj (coseparator C), isCoseparator_coseparator C |>.of_equivalence α⟩

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