setOf_subset_eq_univ_iff — Mathlib

English

For S a theory, the set {p : T.CompleteType α | S ⊆ ↑p} is universal iff every φ ∈ S is realized in some model of T with constants.

Русский

Для теории S множество {p : T.CompleteType α | S ⊆ ↑p} равно все p тогда и только тогда каждый φ ∈ S реализуется в какой-либо модели T.

LaTeX

$$${p : T.CompleteType α | S ⊆ ↑p} = Set.univ \\\\iff \\\\forall φ ∈ S, (L.lhomWithConstants α).onTheory T \\\\models^{\\\\mathrm{b}} φ$$$

Lean4

theorem setOf_subset_eq_univ_iff (S : L[[α]].Theory) :
    {p : T.CompleteType α | S ⊆ ↑p} = Set.univ ↔ ∀ φ, φ ∈ S → (L.lhomWithConstants α).onTheory T ⊨ᵇ φ :=
  by
  have h : {p : T.CompleteType α | S ⊆ ↑p} = ⋂₀ ((fun φ => {p | φ ∈ p}) '' S) :=
    by
    ext
    simp [subset_def]
  simp_rw [h, sInter_eq_univ, ← setOf_mem_eq_univ_iff]
  refine ⟨fun h φ φS => h _ ⟨_, φS, rfl⟩, ?_⟩
  rintro h _ ⟨φ, h1, rfl⟩
  exact h _ h1

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