setOf_mem_eq_univ_iff — Mathlib

English

For any φ, φ ∈ p holds for all p iff φ is realized in some model of T via constants.

Русский

Для любого φ выполнено: φ ∈ p для всех p эквивалентно тому, что φ реализуется в некоторой модели T через константы.

LaTeX

$$${p : T.CompleteType α | φ \\\\in p} = Set.univ \\\\iff (L.lhomWithConstants α).onTheory T \\\\models^{\\\\mathrm{b}} φ$$$

Lean4

theorem setOf_mem_eq_univ_iff (φ : L[[α]].Sentence) :
    {p : T.CompleteType α | φ ∈ p} = Set.univ ↔ (L.lhomWithConstants α).onTheory T ⊨ᵇ φ :=
  by
  rw [models_iff_not_satisfiable, ← compl_empty_iff, compl_setOf_mem, ← setOf_subset_eq_empty_iff]
  simp

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