mem_or_not_mem

Mathlib.ModelTheory.Types

URI: https://scilib.ai/kg/mathlib#FirstOrder.Language.Theory.CompleteType.mem_or_not_mem

English

For any p and sentence φ, either φ ∈ p or φ.not ∈ p.

Русский

Для любого p и предиката φ либо φ ∈ p, либо φ.not ∈ p.

LaTeX

$$$\\\\forall p\\\\forall\\\\phi\\\\ (\\\\phi\\\\in p \\\\lor \\\\phi.not \\\\in p)$$$

Lean4

theorem mem_or_not_mem (p : T.CompleteType α) (φ : L[[α]].Sentence) : φ ∈ p ∨ φ.not ∈ p :=
  p.isMaximal.mem_or_not_mem φ

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

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

Разделы

Аффилиация

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