nonempty_of_nonempty_constants — Mathlib

English

If the language L has a nonempty type of constants, then any L-structure M is nonempty.

Русский

Если язык L имеет непустое множество констант, то любая L-структура M непустая.

LaTeX

$$$\\operatorname{Nonempty}(L.Constants) \\Rightarrow \\operatorname{Nonempty}(M)$$$

Lean4

/-- Given a language with a nonempty type of constants, any structure will be nonempty. This cannot
  be a global instance, because `L` becomes a metavariable. -/
theorem nonempty_of_nonempty_constants [h : Nonempty L.Constants] : Nonempty M :=
  h.map (↑)

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