Theorems · Definition · logic and foundations

FirstOrder.Language.Substructure.withConstants

{L : FirstOrder.Language} →
  {M : Type w} →
    [inst : L.Structure M] → (S : L.Substructure M) → {A : Set M} → A ⊆ ↑S → (L.withConstants ↑A).Substructure M

Turns any substructure containing a constant set A into a L[[A]]-substructure.

Defined in: Mathlib.ModelTheory.Substructures
Cited by: 5 results in Mathlib
Foundations: Depth 20 from the axioms · uses no axioms
Assumes: FirstOrder.Language.Structure

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites8

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
SetLike.coestatement and proof · cited by 8,199
Set.Elemstatement and proof · cited by 7,166
FirstOrder.Languagestatement and proof · cited by 1,084
FirstOrder.Language.Structurestatement and proof · cited by 775
FirstOrder.Language.Substructurestatement and proof · cited by 242
FirstOrder.Language.Functionsproof · cited by 153
FirstOrder.Language.withConstantsstatement and proof · cited by 108

Cited by5

Results whose statement or proof uses this declaration.

FirstOrder.Language.Substructure.reduct_withConstantsstatement · cited by 1
FirstOrder.Language.Substructure.mem_withConstantsstatement · cited by 0
FirstOrder.Language.Substructure.coe_withConstantsstatement · cited by 0
FirstOrder.Language.Substructure.closure_withConstants_eqstatement · cited by 0
FirstOrder.Language.Substructure.withConstants.congr_simpstatement and proof · cited by 0