model_union_iff — Mathlib

English

Two theories T and T' give the same set of models in M iff T and T' are logically equivalent in M.

Русский

Две теории T и T' дают одинаковые множества моделей в M тогда и только тогда они логически эквивалентны в M.

LaTeX

$$$ M \models T \cup T' \iff M \models T \land M \models T' $$$

Lean4

@[simp]
theorem model_union_iff {T' : L.Theory} : M ⊨ T ∪ T' ↔ M ⊨ T ∧ M ⊨ T' :=
  ⟨fun h => ⟨h.mono Set.subset_union_left, h.mono Set.subset_union_right⟩, fun h => h.1.union h.2⟩

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