Hereditary — Mathlib

English

A class K has the hereditary property if whenever a structure M belongs to K, every finitely generated L-substructure that embeds into M also lies in K.

Русский

Класс K наследуем, если для любого M ∈ K все FG-подструктуры, внедряющиеся в M, также принадлежат K.

LaTeX

$$$\text{Hereditary}(K) \;\equiv\; \forall M:\text{Bundled } L\text{Structure},\; M \in K \rightarrow L.\mathrm{age}(M) \subseteq K$$$

Lean4

/-- A class `K` has the hereditary property when all finitely-generated structures that embed into
  structures in `K` are also in `K`. -/
def Hereditary : Prop :=
  ∀ M : Bundled.{w} L.Structure, M ∈ K → L.age M ⊆ K

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