Theorems · Theorem · logic and foundations
FirstOrder.Language.Structure.FG.finite
∀ {L : FirstOrder.Language} {M : Type u_1} [inst : L.Structure M] [L.IsRelational],
FirstOrder.Language.Structure.FG L M → Finite M- Defined in
- Mathlib.ModelTheory.FinitelyGenerated
- Cited by
- 3 results in Mathlib
- Foundations
- Depth 74 from the axioms · uses propext, Classical.choice, Quot.sound
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.
- Finitestatement · cited by 3,029
- FirstOrder.Languagestatement and proof · cited by 1,084
- FirstOrder.Language.Structurestatement and proof · cited by 775
- FirstOrder.Language.Structure.FGstatement and proof · cited by 27
- FirstOrder.Language.IsRelationalstatement and proof · cited by 10
- FirstOrder.Language.Structure.fg_defproof · cited by 6
- Finite.of_finite_univproof · cited by 4
- FirstOrder.Language.Substructure.FG.finiteproof · cited by 3
Cited by3
Results whose statement or proof uses this declaration.
- FirstOrder.Language.dlo_ageproof · cited by 1
- FirstOrder.Language.dlo_isExtensionPairproof · cited by 1
- FirstOrder.Language.Structure.fg_iff_finiteproof · cited by 0