toList_foldr_inf_mem — Mathlib

English

Let p be a complete type and t a finite list of sentences. The conjunction of t lies in p iff t, as a set of sentences, is contained in p.

Русский

Пусть p — полный тип, а t — конечный список предложений. Конъюнкция предложений в t принадлежит p тогда и только тогда, когда множество предложений t содержится в p.

LaTeX

$$$t.toList.foldr (\\\\wedge) \\\\top \\\\in p \\\\iff (t : L[[\\\\alpha]]).Theory \\\\subseteq ↑p$$$

Lean4

theorem toList_foldr_inf_mem {p : T.CompleteType α} {t : Finset (L[[α]]).Sentence} :
    t.toList.foldr (· ⊓ ·) ⊤ ∈ p ↔ (t : L[[α]].Theory) ⊆ ↑p :=
  by
  simp_rw [subset_def, ← SetLike.mem_coe, p.isMaximal.mem_iff_models, models_sentence_iff, Sentence.Realize,
    Formula.Realize, BoundedFormula.realize_foldr_inf, Finset.mem_toList]
  exact ⟨fun h φ hφ M => h _ _ hφ, fun h M φ hφ => h _ hφ _⟩

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