Theorems · Definition · logic and foundations
FirstOrder.Language.ClosedUnder
{L : FirstOrder.Language} → {M : Type w} → [L.Structure M] → {n : ℕ} → L.Functions n → Set M → PropIndicates that a set in a given structure is a closed under a function symbol.
- Defined in
- Mathlib.ModelTheory.Substructures
- Cited by
- 13 results in Mathlib
- Foundations
- Depth 4 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
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
- FirstOrder.Languagestatement and proof · cited by 1,084
- FirstOrder.Language.Structurestatement and proof · cited by 775
- FirstOrder.Language.Functionsstatement and proof · cited by 153
- FirstOrder.Language.Structure.funMapproof · cited by 69
Cited by18
Results whose statement or proof uses this declaration.
- FirstOrder.Language.Substructure.fun_memstatement · cited by 5
- FirstOrder.Language.Substructure.closure_inductionstatement and proof · cited by 3
- FirstOrder.Language.Substructure.mk.injstatement and proof · cited by 1
- FirstOrder.Language.Substructure.mk.noConfusionstatement and proof · cited by 1
- FirstOrder.Language.ClosedUnder.interstatement and proof · cited by 1
- FirstOrder.Language.Substructure.mem_closed_iffstatement and proof · cited by 1
- FirstOrder.Language.Substructure.noConfusionproof · cited by 0
- FirstOrder.Language.Substructure.noConfusionTypeproof · cited by 0
- FirstOrder.Language.Substructure.recOnstatement and proof · cited by 0
- FirstOrder.Language.Substructure.closure_induction'statement and proof · cited by 0
- FirstOrder.Language.Substructure.mk.congr_simpstatement and proof · cited by 0
- FirstOrder.Language.Substructure.mk.injEqstatement and proof · cited by 0