Theorems · Definition · logic and foundations
FirstOrder.Language.Equiv.toEquiv
{L : FirstOrder.Language} →
{M : Type w} → {N : Type w'} → [inst : L.Structure M] → [inst_1 : L.Structure N] → L.Equiv M N → M ≃ N- Defined in
- Mathlib.ModelTheory.Basic
- Cited by
- 12 results in Mathlib
- Foundations
- Depth 3 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Equivstatement · cited by 8,337
- FirstOrder.Languagestatement and proof · cited by 1,084
- FirstOrder.Language.Structurestatement and proof · cited by 775
- FirstOrder.Language.Equivstatement and proof · cited by 83
Cited by15
Results whose statement or proof uses this declaration.
- FirstOrder.Language.Equiv.symmproof · cited by 32
- FirstOrder.Language.Equiv.compproof · cited by 12
- FirstOrder.Language.Equiv.apply_symm_applyproof · cited by 6
- FirstOrder.Language.Equiv.symm_apply_applyproof · cited by 3
- FirstOrder.Language.Equiv.fg_iffproof · cited by 3
- FirstOrder.Language.empty.isFraisseLimit_of_countable_infiniteproof · cited by 1
- FirstOrder.Language.empty.nonempty_equiv_iffproof · cited by 1
- FirstOrder.Language.Structure.cg_iff_countableproof · cited by 1
- FirstOrder.Language.Embedding.equivRange_toEquiv_applystatement and proof · cited by 1
- FirstOrder.Ring.languageEquivEquivRingEquivproof · cited by 1
- FirstOrder.Language.Equiv.cg_iffproof · cited by 0
- FirstOrder.Language.StrongHomClass.toEquiv_invFunstatement and proof · cited by 0