mem_of_models — Mathlib

English

If T is maximal and φ is realized in all models of T, then φ ∈ T.

Русский

Если T максимальна и φ реализуется во всех моделях T, то φ ∈ T.

LaTeX

$$$\\text{iff } φ \\in T$ given $T$ maximal and $T \\models^b φ$$$

Lean4

theorem mem_of_models (h : T.IsMaximal) {φ : L.Sentence} (hφ : T ⊨ᵇ φ) : φ ∈ T :=
  by
  refine (h.mem_or_not_mem φ).resolve_right fun con => ?_
  rw [models_iff_not_satisfiable, Set.union_singleton, Set.insert_eq_of_mem con] at hφ
  exact hφ h.1

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