subobjectEquivSet — Mathlib

English

For any α, Subobject α is order-isomorphic to Set α; i.e., subobjects of α correspond to subsets of α.

Русский

Для любого α Subobject α эквивалентен порядочно, как Set α; т.е. подобъекты α соответствуют подмножествам α.

LaTeX

$$$\mathrm{Subobject}(\alpha) \cong_o \mathrm{Set}(\alpha).$$$

Lean4

/-- For `α : Type u`, `Subobject α` is order isomorphic to `Set α`.
-/
noncomputable def subobjectEquivSet (α : Type u) : Subobject α ≃o Set α :=
  (Types.monoOverEquivalenceSet α).thinSkeletonOrderIso

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