of_equivalence — Mathlib

English

If G is a separator and α: C ≌ D is an equivalence, then α(G) is a separator.

Русский

Если G является сепаратором, и существует эквиваленция α: C ≌ D, то образ α(G) является сепаратором.

LaTeX

$$$$\text{IsSeparator}(G) \Rightarrow \text{IsSeparator}(\alpha(G)).$$$$

Lean4

theorem of_equivalence {G : C} (h : IsSeparator G) (α : C ≌ D) : IsSeparator (α.functor.obj G) := by
  simpa using IsSeparating.of_equivalence h α

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