small — Mathlib

English

If X is u-small, then Xᵒᵖ is u-small.

Русский

Если X является u-малым, то Xᵒᵖ тоже является u-малым.

LaTeX

$$$$ \operatorname{Small}(X) \Rightarrow \operatorname{Small}(X^{op}) $$$$

Lean4

/-- If `X` is `u`-small, also `Xᵒᵖ` is `u`-small. -/
instance small {X : Type v} [Small.{u} X] : Small.{u} Xᵒᵖ :=
  by
  obtain ⟨S, ⟨e⟩⟩ := Small.equiv_small (α := X)
  exact ⟨S, ⟨equivToOpposite.symm.trans e⟩⟩

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