nonempty — Mathlib

English

The age of a structure is always nonempty; there exists a finitely generated substructure embedding into the structure.

Русский

Возраст структуры всегда непуст; существует FG-подструктура, внедряющаяся в данную структуру.

LaTeX

$$$(L.age M).Nonempty$$$

Lean4

theorem nonempty : (L.age M).Nonempty :=
  ⟨Bundled.of (Substructure.closure L (∅ : Set M)), (fg_iff_structure_fg _).1 (fg_closure Set.finite_empty),
    ⟨Substructure.subtype _⟩⟩

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