Theorems · Theorem · logic and foundations

FirstOrder.Language.Theory.CompleteType.toList_foldr_inf_mem

∀ {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {p : T.CompleteType α}
  {t : Finset (L.withConstants α).Sentence}, List.foldr (fun x1 x2 => x1 ⊓ x2) ⊤ t.toList ∈ p ↔ ↑t ⊆ ↑p

Defined in

Mathlib.ModelTheory.Types

Cited by

0 results in Mathlib

Foundations

Depth 56 from the axioms · uses propext, Classical.choice, Quot.sound