Theorems · Definition · logic and foundations
FirstOrder.Language.FGEquiv
(L : FirstOrder.Language) → (M : Type w) → (N : Type w') → [L.Structure M] → [L.Structure N] → Type (max 0 w w')
The type of equivalences between finitely generated substructures.
- Defined in
- Mathlib.ModelTheory.PartialEquiv
- Cited by
- 9 results in Mathlib
- Foundations
- Depth 70 from the axioms · uses propext, Classical.choice, Quot.sound
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.
- FirstOrder.Languagestatement and proof · cited by 1,084
- FirstOrder.Language.Structurestatement and proof · cited by 775
- FirstOrder.Language.PartialEquivproof · cited by 44
- FirstOrder.Language.PartialEquiv.domproof · cited by 35
- FirstOrder.Language.Substructure.FGproof · cited by 34
Cited by13
Results whose statement or proof uses this declaration.
- FirstOrder.Language.IsExtensionPairproof · cited by 8
- FirstOrder.Language.IsExtensionPair.definedAtLeftstatement and proof · cited by 2
- FirstOrder.Language.FGEquiv.symmstatement and proof · cited by 2
- FirstOrder.Language.equiv_between_cgstatement and proof · cited by 2
- FirstOrder.Language.IsExtensionPair.definedAtRightstatement and proof · cited by 1
- FirstOrder.Language.isExtensionPair_iff_codstatement and proof · cited by 1
- FirstOrder.Language.isUltrahomogeneous_iff_IsExtensionPairproof · cited by 1
- FirstOrder.Language.IsFraisseLimit.isExtensionPairproof · cited by 1
- FirstOrder.Language.countable_self_fgequiv_of_countablestatement and proof · cited by 0
- FirstOrder.Language.IsExtensionPair.codstatement · cited by 0
- FirstOrder.Language.FGEquiv.symm_coestatement and proof · cited by 0