coeSort_elementarySkolem₁Reduct

English

There exists a small elementary substructure of M.

Русский

У каждой L-структуры M существует элементарная подструктура S, которая мала по сущности (напр., в пределах малого множества).

LaTeX

$$Exists S : L.ElementarySubstructure M, Small S$$

Lean4

theorem coeSort_elementarySkolem₁Reduct (S : (L.sum L.skolem₁).Substructure M) :
    (S.elementarySkolem₁Reduct : Type w) = S :=
  rfl

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