model_insert_iff — Mathlib

English

Insertion of a sentence φ into a theory T is realized exactly when φ and T are both realized.

Русский

Вставка предложения φ в теорию T реализуется тогда и только тогда, когда реализуются и φ, и T.

LaTeX

$$$ M \models insert(\varphi, T) \iff M \models \varphi \land M \models T $$$

Lean4

theorem model_insert_iff {φ : L.Sentence} : M ⊨ insert φ T ↔ M ⊨ φ ∧ M ⊨ T := by
  rw [Set.insert_eq, model_union_iff, model_singleton_iff]

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