mem_top

Mathlib.ModelTheory.ElementarySubstructures

URI: https://scilib.ai/kg/mathlib#FirstOrder.Language.ElementarySubstructure.mem_top

English

Every element of M lies in the top elementary substructure.

Русский

Каждый элемент M принадлежит вершине элементарной подструктуры.

LaTeX

$$$\forall x \in M,\ x \in \top$$$

Lean4

@[simp]
theorem mem_top (x : M) : x ∈ (⊤ : L.ElementarySubstructure M) :=
  Set.mem_univ x

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru