exists_small_elementarySubstructure

English

There exists a small elementary substructure.

Русский

Существует маленькая элементарная подструктура M, которая находится в пределах заданной вселенной.

LaTeX

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

Lean4

theorem exists_small_elementarySubstructure : ∃ S : L.ElementarySubstructure M, Small.{max u v} S :=
  ⟨Substructure.elementarySkolem₁Reduct ⊥, inferInstance⟩

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