realize_bot

Mathlib.ModelTheory.Semantics

URI: https://scilib.ai/kg/mathlib#FirstOrder.Language.Formula.realize_bot

English

The realization of all (liftAt 1 n φ) coincides with the realization of φ when the domain is nonempty.

Русский

Реализация all (liftAt 1 n φ) совпадает с реализацией φ при непустом домене.

LaTeX

$$$ (\text{liftAt 1 n } φ)^{\mathcal{M}}.\text{all.Realize}(v, xs) \iff φ^{\mathcal{M}}(v, xs) $$$

Lean4

@[simp]
theorem realize_bot : (⊥ : L.Formula α).Realize v ↔ False :=
  Iff.rfl

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

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

Разделы

Аффилиация

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