essentiallySmall_congr — Mathlib

English

If C ≌ D, then C is essentially small iff D is essentially small.

Русский

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

LaTeX

$$$\operatorname{EssentiallySmall}(C) \iff \operatorname{EssentiallySmall}(D)$$$

Lean4

theorem essentiallySmall_congr {C : Type u} [Category.{v} C] {D : Type u'} [Category.{v'} D] (e : C ≌ D) :
    EssentiallySmall.{w} C ↔ EssentiallySmall.{w} D :=
  by
  fconstructor
  · rintro ⟨S, 𝒮, ⟨f⟩⟩
    exact EssentiallySmall.mk' (e.symm.trans f)
  · rintro ⟨S, 𝒮, ⟨f⟩⟩
    exact EssentiallySmall.mk' (e.trans f)

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