realize_sentence_of_mem — Mathlib

English

Every structure M satisfies the empty theory, i.e., all formulas in the empty theory hold vacuously.

Русский

Любая структура M удовлетворяет пустой теории, то есть все формулы пустой теории истинны по необходимости.

LaTeX

$$$ M \models \emptyset \quad\text{(theory)} $$$

Lean4

theorem realize_sentence_of_mem [M ⊨ T] {φ : L.Sentence} (h : φ ∈ T) : M ⊨ φ :=
  Theory.Model.realize_of_mem φ h

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