Mathlib Map

Theorems · Inductive type · logic and foundations

FirstOrder.Language.StrongHomClass

(L : outParam FirstOrder.Language) →
  (F : Type u_3) →
    (M : outParam (Type u_4)) → (N : outParam (Type u_5)) → [FunLike F M N] → [L.Structure M] → [L.Structure N] → Prop

StrongHomClass L F M N states that F is a type of L-homomorphisms which preserve relations in both directions.

Defined in
Mathlib.ModelTheory.Basic
Cited by
16 results in Mathlib
Foundations
Depth 3 from the axioms · uses no axioms
Assumes
FunLikeFirstOrder.Language.StructureFirstOrder.Language.Structure
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

FirstOrder.Language.StrongHomClass.map_rel · cited by 5StrongHomClass.map_relFirstOrder.Language.StrongHomClass.toEmbedding · cited by 4StrongHomClass.toEmbeddingFirstOrder.Language.StrongHomClass.toEquiv · cited by 4StrongHomClass.toEquivFirstOrder.Language.StrongHomClass.realize_sentence · cited by 3StrongHomClass.realize_se…FirstOrder.Language.BoundedFormula.IsQF.realize_embedding · cited by 2IsQF.realize_embeddingFirstOrder.Language.StrongHomClass.realize_boundedFormula · cited by 2StrongHomClass.realize_bo…FirstOrder.Language.StrongHomClass.realize_formula · cited by 2StrongHomClass.realize_fo…FirstOrder.Language.BoundedFormula.IsUniversal.realize_embedding · cited by 1IsUniversal.realize_embed…FirstOrder.Language.StrongHomClass.toEquiv_toFun · cited by 1StrongHomClass.toEquiv_to…FirstOrder.Language.HomClass.strongHomClassOfIsAlgebraic · cited by 0HomClass.strongHomClassOf…FirstOrder.Language.StrongHomClass.casesOn · cited by 0StrongHomClass.casesOnFirstOrder.Language.StrongHomClass.elementarilyEquivalent · cited by 0StrongHomClass.elementari…FirstOrder.Language.StrongHomClass.map_fun · cited by 0StrongHomClass.map_funFirstOrder.Language.StrongHomClass.toEquiv.congr_simp · cited by 0toEquiv.congr_simpFirstOrder.Language.StrongHomClass.recOn · cited by 0StrongHomClass.recOnFunLike · cited by 2560FunLikeFirstOrder.Language · cited by 1084FirstOrder.LanguageFirstOrder.Language.Structure · cited by 775Language.StructureLanguage.StrongHomClassCITED BYCITES

Cites3

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by20

Results whose statement or proof uses this declaration.