Theorems · Theorem · logic and foundations

FirstOrder.Language.distinctConstantsTheory_eq_iUnion

∀ {L : FirstOrder.Language} {α : Type u'} (s : Set α),
  L.distinctConstantsTheory s =
    ⋃ t, L.distinctConstantsTheory ↑(Finset.map (Function.Embedding.subtype fun x => x ∈ s) t)

Defined in: Mathlib.ModelTheory.Syntax
Cited by: 1 results in Mathlib
Foundations: Depth 61 from the axioms · uses propext, Classical.choice, Quot.sound

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites24

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Setstatement and proof · cited by 53,352
Finsetstatement and proof · cited by 13,712
SetLike.coestatement and proof · cited by 8,199
Set.Elemstatement and proof · cited by 7,166
Set.imageproof · cited by 5,609
Compl.complproof · cited by 2,925
Set.iUnionstatement and proof · cited by 2,483
Set.extproof · cited by 2,266
SProd.sprodproof · cited by 1,750
FirstOrder.Languagestatement and proof · cited by 1,084
Finset.mapstatement and proof · cited by 747
FirstOrder.Language.Theorystatement · cited by 154

Cited by1

Results whose statement or proof uses this declaration.

FirstOrder.Language.Theory.isSatisfiable_union_distinctConstantsTheory_of_infiniteproof · cited by 1