instNonempty — Mathlib

English

If X is nonempty, then the action category ActionCategory(M,X) is nonempty; in particular, there exists at least one object in the category.

Русский

Если X непусто, то категория действий ActionCategory(M,X) ненулевая; то есть существует хотя бы один объект в этой категории.

LaTeX

$$$\operatorname{Nonempty}(X) \Rightarrow \operatorname{Nonempty}(\mathsf{ActionCategory}(M,X))$$$

Lean4

instance [Nonempty X] : Nonempty (ActionCategory M X) :=
  Nonempty.map (objEquiv M X) inferInstance

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