mathlib documentation

model_theory.basic

Basics on First-Order Structures #

This file defines first-order languages and structures in the style of the Flypitch project, as well as several important maps between structures.

Main Definitions #

TODO #

Use [countable L.symbols] instead of [L.countable].

References #

For the Flypitch project:

Languages and Structures #

@[nolint]
structure first_order.language  :
Type (max (u+1) (v+1))
  • functions : Type ?
  • relations : Type ?

A first-order language consists of a type of functions of every natural-number arity and a type of relations of every natural-number arity.

Instances for first_order.language
@[simp]
def first_order.sequence₂ (a₀ a₁ a₂ : Type u) :
Type u

Used to define first_order.language₂.

Equations
Instances for first_order.sequence₂
@[protected, instance]
def first_order.sequence₂.inhabited₀ (a₀ a₁ a₂ : Type u) [h : inhabited a₀] :
Equations
@[protected, instance]
def first_order.sequence₂.inhabited₁ (a₀ a₁ a₂ : Type u) [h : inhabited a₁] :
Equations
@[protected, instance]
def first_order.sequence₂.inhabited₂ (a₀ a₁ a₂ : Type u) [h : inhabited a₂] :
Equations
@[protected, instance]
def first_order.sequence₂.is_empty (a₀ a₁ a₂ : Type u) {n : } :
is_empty (first_order.sequence₂ a₀ a₁ a₂ (n + 3))
@[simp]
theorem first_order.sequence₂.lift_mk (a₀ a₁ a₂ : Type u) {i : } :
@[simp]
theorem first_order.sequence₂.sum_card (a₀ a₁ a₂ : Type u) :
@[simp]
theorem first_order.language.mk₂_relations (c f₁ f₂ : Type u) (r₁ r₂ : Type v) (ᾰ : ) :
(first_order.language.mk₂ c f₁ f₂ r₁ r₂).relations = first_order.sequence₂ pempty r₁ r₂
@[simp]
theorem first_order.language.mk₂_functions (c f₁ f₂ : Type u) (r₁ r₂ : Type v) (ᾰ : ) :
(first_order.language.mk₂ c f₁ f₂ r₁ r₂).functions = first_order.sequence₂ c f₁ f₂
@[protected]
def first_order.language.mk₂ (c f₁ f₂ : Type u) (r₁ r₂ : Type v) :

A constructor for languages with only constants, unary and binary functions, and unary and binary relations.

Equations
Instances for first_order.language.mk₂
@[protected]

The sum of two languages consists of the disjoint union of their symbols.

Equations
Instances for first_order.language.sum
@[protected, nolint]

The type of constants in a given language.

Equations
Instances for first_order.language.constants
@[simp]
theorem first_order.language.constants_mk₂ (c f₁ f₂ : Type u) (r₁ r₂ : Type v) :
(first_order.language.mk₂ c f₁ f₂ r₁ r₂).constants = c
@[nolint]

The type of symbols in a given language.

Equations
Instances for first_order.language.symbols

The cardinality of a language is the cardinality of its type of symbols.

Equations
@[protected, instance]
@[protected, instance]
@[protected, instance]
def first_order.language.is_relational_mk₂ {c f₁ f₂ : Type u} {r₁ r₂ : Type v} [h0 : is_empty c] [h1 : is_empty f₁] [h2 : is_empty f₂] :
@[protected, instance]
def first_order.language.is_algebraic_mk₂ {c f₁ f₂ : Type u} {r₁ r₂ : Type v} [h1 : is_empty r₁] [h2 : is_empty r₂] :
@[protected, instance]
def first_order.language.subsingleton_mk₂_functions {c f₁ f₂ : Type u} {r₁ r₂ : Type v} [h0 : subsingleton c] [h1 : subsingleton f₁] [h2 : subsingleton f₂] {n : } :
@[protected, instance]
def first_order.language.subsingleton_mk₂_relations {c f₁ f₂ : Type u} {r₁ r₂ : Type v} [h1 : subsingleton r₁] [h2 : subsingleton r₂] {n : } :
@[simp]
theorem first_order.language.card_mk₂ (c f₁ f₂ : Type u) (r₁ r₂ : Type v) :
@[ext, class]
structure first_order.language.Structure (L : first_order.language) (M : Type w) :
Type (max u v w)

A first-order structure on a type M consists of interpretations of all the symbols in a given language. Each function of arity n is interpreted as a function sending tuples of length n (modeled as (fin n → M)) to M, and a relation of arity n is a function from tuples of length n to Prop.

Instances of this typeclass
Instances of other typeclasses for first_order.language.Structure

Maps #

structure first_order.language.hom (L : first_order.language) (M : Type w) (N : Type w') [L.Structure M] [L.Structure N] :
Type (max w w')

A homomorphism between first-order structures is a function that commutes with the interpretations of functions and maps tuples in one structure where a given relation is true to tuples in the second structure where that relation is still true.

Instances for first_order.language.hom
structure first_order.language.embedding (L : first_order.language) (M : Type w) (N : Type w') [L.Structure M] [L.Structure N] :
Type (max w w')

An embedding of first-order structures is an embedding that commutes with the interpretations of functions and relations.

Instances for first_order.language.embedding
structure first_order.language.equiv (L : first_order.language) (M : Type w) (N : Type w') [L.Structure M] [L.Structure N] :
Type (max w w')

An equivalence of first-order structures is an equivalence that commutes with the interpretations of functions and relations.

Instances for first_order.language.equiv

Given a language with a nonempty type of constants, any structure will be nonempty. This cannot be a global instance, because L becomes a metavariable.

def first_order.language.fun_map₂ {M : Type w} {c f₁ f₂ : Type u} {r₁ r₂ : Type v} (c' : c → M) (f₁' : f₁ → M → M) (f₂' : f₂ → M → M → M) {n : } :
(first_order.language.mk₂ c f₁ f₂ r₁ r₂).functions n(fin n → M) → M

The function map for first_order.language.Structure₂.

Equations
def first_order.language.rel_map₂ {M : Type w} {c f₁ f₂ : Type u} {r₁ r₂ : Type v} (r₁' : r₁ → set M) (r₂' : r₂ → M → M → Prop) {n : } :
(first_order.language.mk₂ c f₁ f₂ r₁ r₂).relations n(fin n → M) → Prop

The relation map for first_order.language.Structure₂.

Equations
@[protected]
def first_order.language.Structure.mk₂ {M : Type w} {c f₁ f₂ : Type u} {r₁ r₂ : Type v} (c' : c → M) (f₁' : f₁ → M → M) (f₂' : f₂ → M → M → M) (r₁' : r₁ → set M) (r₂' : r₂ → M → M → Prop) :
(first_order.language.mk₂ c f₁ f₂ r₁ r₂).Structure M

A structure constructor to match first_order.language₂.

Equations
@[simp]
theorem first_order.language.Structure.fun_map_apply₀ {M : Type w} {c f₁ f₂ : Type u} {r₁ r₂ : Type v} {c' : c → M} {f₁' : f₁ → M → M} {f₂' : f₂ → M → M → M} {r₁' : r₁ → set M} {r₂' : r₂ → M → M → Prop} (c₀ : c) {x : fin 0 → M} :
@[simp]
theorem first_order.language.Structure.fun_map_apply₁ {M : Type w} {c f₁ f₂ : Type u} {r₁ r₂ : Type v} {c' : c → M} {f₁' : f₁ → M → M} {f₂' : f₂ → M → M → M} {r₁' : r₁ → set M} {r₂' : r₂ → M → M → Prop} (f : f₁) (x : M) :
@[simp]
theorem first_order.language.Structure.fun_map_apply₂ {M : Type w} {c f₁ f₂ : Type u} {r₁ r₂ : Type v} {c' : c → M} {f₁' : f₁ → M → M} {f₂' : f₂ → M → M → M} {r₁' : r₁ → set M} {r₂' : r₂ → M → M → Prop} (f : f₂) (x y : M) :
@[simp]
theorem first_order.language.Structure.rel_map_apply₁ {M : Type w} {c f₁ f₂ : Type u} {r₁ r₂ : Type v} {c' : c → M} {f₁' : f₁ → M → M} {f₂' : f₂ → M → M → M} {r₁' : r₁ → set M} {r₂' : r₂ → M → M → Prop} (r : r₁) (x : M) :
@[simp]
theorem first_order.language.Structure.rel_map_apply₂ {M : Type w} {c f₁ f₂ : Type u} {r₁ r₂ : Type v} {c' : c → M} {f₁' : f₁ → M → M} {f₂' : f₂ → M → M → M} {r₁' : r₁ → set M} {r₂' : r₂ → M → M → Prop} (r : r₂) (x y : M) :
@[class]
structure first_order.language.hom_class (L : out_param first_order.language) (F : Type u_5) (M : out_param (Type u_6)) (N : out_param (Type u_7)) [fun_like F M (λ (_x : M), N)] [first_order.language.Structure L M] [first_order.language.Structure L N] :
Type

hom_class L F M N states that F is a type of L-homomorphisms. You should extend this typeclass when you extend first_order.language.hom.

Instances of this typeclass
Instances of other typeclasses for first_order.language.hom_class
  • first_order.language.hom_class.has_sizeof_inst
@[class]
structure first_order.language.strong_hom_class (L : out_param first_order.language) (F : Type u_5) (M : out_param (Type u_6)) (N : out_param (Type u_7)) [fun_like F M (λ (_x : M), N)] [first_order.language.Structure L M] [first_order.language.Structure L N] :
Type

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

Instances of this typeclass
Instances of other typeclasses for first_order.language.strong_hom_class
  • first_order.language.strong_hom_class.has_sizeof_inst
@[protected, instance]
def first_order.language.strong_hom_class.hom_class {L : first_order.language} {F : Type u_1} {M : Type u_2} {N : Type u_3} [L.Structure M] [L.Structure N] [fun_like F M (λ (_x : M), N)] [first_order.language.strong_hom_class L F M N] :
Equations

Not an instance to avoid a loop.

Equations
theorem first_order.language.hom_class.map_constants {L : first_order.language} {F : Type u_1} {M : Type u_2} {N : Type u_3} [L.Structure M] [L.Structure N] [fun_like F M (λ (_x : M), N)] [first_order.language.hom_class L F M N] (φ : F) (c : L.constants) :
φ c = c
@[protected, instance]
def first_order.language.hom.fun_like {L : first_order.language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] :
fun_like (L.hom M N) M (λ (_x : M), N)
Equations
@[protected, instance]
def first_order.language.hom.hom_class {L : first_order.language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] :
Equations
@[protected, instance]
def first_order.language.hom.has_coe_to_fun {L : first_order.language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] :
has_coe_to_fun (L.hom M N) (λ (_x : L.hom M N), M → N)
Equations
@[simp]
theorem first_order.language.hom.to_fun_eq_coe {L : first_order.language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {f : L.hom M N} :
@[ext]
theorem first_order.language.hom.ext {L : first_order.language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] ⦃f g : L.hom M N⦄ (h : ∀ (x : M), f x = g x) :
f = g
theorem first_order.language.hom.ext_iff {L : first_order.language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {f g : L.hom M N} :
f = g ∀ (x : M), f x = g x
@[simp]
theorem first_order.language.hom.map_fun {L : first_order.language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (φ : L.hom M N) {n : } (f : L.functions n) (x : fin n → M) :
@[simp]
theorem first_order.language.hom.map_constants {L : first_order.language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (φ : L.hom M N) (c : L.constants) :
φ c = c
@[simp]
theorem first_order.language.hom.map_rel {L : first_order.language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (φ : L.hom M N) {n : } (r : L.relations n) (x : fin n → M) :
@[refl]
def first_order.language.hom.id (L : first_order.language) (M : Type w) [L.Structure M] :
L.hom M M

The identity map from a structure to itself

Equations
@[simp]
@[trans]
def first_order.language.hom.comp {L : first_order.language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {P : Type u_1} [L.Structure P] (hnp : L.hom N P) (hmn : L.hom M N) :
L.hom M P

Composition of first-order homomorphisms

Equations
@[simp]
theorem first_order.language.hom.comp_apply {L : first_order.language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {P : Type u_1} [L.Structure P] (g : L.hom N P) (f : L.hom M N) (x : M) :
(g.comp f) x = g (f x)
theorem first_order.language.hom.comp_assoc {L : first_order.language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {P : Type u_1} [L.Structure P] {Q : Type u_2} [L.Structure Q] (f : L.hom M N) (g : L.hom N P) (h : L.hom P Q) :
(h.comp g).comp f = h.comp (g.comp f)

Composition of first-order homomorphisms is associative.

def first_order.language.hom_class.to_hom {L : first_order.language} {F : Type u_1} {M : Type u_2} {N : Type u_3} [L.Structure M] [L.Structure N] [fun_like F M (λ (_x : M), N)] [first_order.language.hom_class L F M N] :
F → L.hom M N

Any element of a hom_class can be realized as a first_order homomorphism.

Equations
@[protected, instance]
def first_order.language.embedding.embedding_like {L : first_order.language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] :
Equations
@[protected, instance]
def first_order.language.embedding.has_coe_to_fun {L : first_order.language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] :
has_coe_to_fun (L.embedding M N) (λ (_x : L.embedding M N), M → N)
Equations
@[simp]
theorem first_order.language.embedding.map_fun {L : first_order.language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (φ : L.embedding M N) {n : } (f : L.functions n) (x : fin n → M) :
@[simp]
theorem first_order.language.embedding.map_constants {L : first_order.language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (φ : L.embedding M N) (c : L.constants) :
φ c = c
@[simp]
theorem first_order.language.embedding.map_rel {L : first_order.language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (φ : L.embedding M N) {n : } (r : L.relations n) (x : fin n → M) :
def first_order.language.embedding.to_hom {L : first_order.language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] :
L.embedding M NL.hom M N

A first-order embedding is also a first-order homomorphism.

Equations
@[simp]
theorem first_order.language.embedding.coe_to_hom {L : first_order.language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {f : L.embedding M N} :
@[ext]
theorem first_order.language.embedding.ext {L : first_order.language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] ⦃f g : L.embedding M N⦄ (h : ∀ (x : M), f x = g x) :
f = g
theorem first_order.language.embedding.ext_iff {L : first_order.language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {f g : L.embedding M N} :
f = g ∀ (x : M), f x = g x
theorem first_order.language.embedding.injective {L : first_order.language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (f : L.embedding M N) :
def first_order.language.embedding.of_injective {L : first_order.language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] [L.is_algebraic] {f : L.hom M N} (hf : function.injective f) :
L.embedding M N

In an algebraic language, any injective homomorphism is an embedding.

Equations
@[refl]

The identity embedding from a structure to itself

Equations
@[trans]
def first_order.language.embedding.comp {L : first_order.language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {P : Type u_1} [L.Structure P] (hnp : L.embedding N P) (hmn : L.embedding M N) :
L.embedding M P

Composition of first-order embeddings

Equations
@[simp]
theorem first_order.language.embedding.comp_apply {L : first_order.language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {P : Type u_1} [L.Structure P] (g : L.embedding N P) (f : L.embedding M N) (x : M) :
(g.comp f) x = g (f x)
theorem first_order.language.embedding.comp_assoc {L : first_order.language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {P : Type u_1} [L.Structure P] {Q : Type u_2} [L.Structure Q] (f : L.embedding M N) (g : L.embedding N P) (h : L.embedding P Q) :
(h.comp g).comp f = h.comp (g.comp f)

Composition of first-order embeddings is associative.

@[simp]
theorem first_order.language.embedding.comp_to_hom {L : first_order.language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {P : Type u_1} [L.Structure P] (hnp : L.embedding N P) (hmn : L.embedding M N) :
(hnp.comp hmn).to_hom = hnp.to_hom.comp hmn.to_hom
def first_order.language.strong_hom_class.to_embedding {L : first_order.language} {F : Type u_1} {M : Type u_2} {N : Type u_3} [L.Structure M] [L.Structure N] [embedding_like F M N] [first_order.language.strong_hom_class L F M N] :
F → L.embedding M N

Any element of an injective strong_hom_class can be realized as a first_order embedding.

Equations
@[protected, instance]
def first_order.language.equiv.equiv_like {L : first_order.language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] :
equiv_like (L.equiv M N) M N
Equations
@[symm]
def first_order.language.equiv.symm {L : first_order.language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (f : L.equiv M N) :
L.equiv N M

The inverse of a first-order equivalence is a first-order equivalence.

Equations
@[protected, instance]
def first_order.language.equiv.has_coe_to_fun {L : first_order.language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] :
has_coe_to_fun (L.equiv M N) (λ (_x : L.equiv M N), M → N)
Equations
@[simp]
theorem first_order.language.equiv.apply_symm_apply {L : first_order.language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (f : L.equiv M N) (a : N) :
f ((f.symm) a) = a
@[simp]
theorem first_order.language.equiv.symm_apply_apply {L : first_order.language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (f : L.equiv M N) (a : M) :
(f.symm) (f a) = a
@[simp]
theorem first_order.language.equiv.map_fun {L : first_order.language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (φ : L.equiv M N) {n : } (f : L.functions n) (x : fin n → M) :
@[simp]
theorem first_order.language.equiv.map_constants {L : first_order.language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (φ : L.equiv M N) (c : L.constants) :
φ c = c
@[simp]
theorem first_order.language.equiv.map_rel {L : first_order.language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (φ : L.equiv M N) {n : } (r : L.relations n) (x : fin n → M) :
def first_order.language.equiv.to_embedding {L : first_order.language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] :
L.equiv M NL.embedding M N

A first-order equivalence is also a first-order embedding.

Equations
def first_order.language.equiv.to_hom {L : first_order.language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] :
L.equiv M NL.hom M N

A first-order equivalence is also a first-order homomorphism.

Equations
@[simp]
theorem first_order.language.equiv.to_embedding_to_hom {L : first_order.language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (f : L.equiv M N) :
@[simp]
theorem first_order.language.equiv.coe_to_hom {L : first_order.language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {f : L.equiv M N} :
@[simp]
theorem first_order.language.equiv.coe_to_embedding {L : first_order.language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (f : L.equiv M N) :
@[ext]
theorem first_order.language.equiv.ext {L : first_order.language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] ⦃f g : L.equiv M N⦄ (h : ∀ (x : M), f x = g x) :
f = g
theorem first_order.language.equiv.ext_iff {L : first_order.language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {f g : L.equiv M N} :
f = g ∀ (x : M), f x = g x
theorem first_order.language.equiv.bijective {L : first_order.language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (f : L.equiv M N) :
theorem first_order.language.equiv.injective {L : first_order.language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (f : L.equiv M N) :
theorem first_order.language.equiv.surjective {L : first_order.language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (f : L.equiv M N) :
@[refl]

The identity equivalence from a structure to itself

Equations
@[trans]
def first_order.language.equiv.comp {L : first_order.language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {P : Type u_1} [L.Structure P] (hnp : L.equiv N P) (hmn : L.equiv M N) :
L.equiv M P

Composition of first-order equivalences

Equations
@[simp]
theorem first_order.language.equiv.comp_apply {L : first_order.language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {P : Type u_1} [L.Structure P] (g : L.equiv N P) (f : L.equiv M N) (x : M) :
(g.comp f) x = g (f x)
theorem first_order.language.equiv.comp_assoc {L : first_order.language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {P : Type u_1} [L.Structure P] {Q : Type u_2} [L.Structure Q] (f : L.equiv M N) (g : L.equiv N P) (h : L.equiv P Q) :
(h.comp g).comp f = h.comp (g.comp f)

Composition of first-order homomorphisms is associative.

def first_order.language.strong_hom_class.to_equiv {L : first_order.language} {F : Type u_1} {M : Type u_2} {N : Type u_3} [L.Structure M] [L.Structure N] [equiv_like F M N] [first_order.language.strong_hom_class L F M N] :
F → L.equiv M N

Any element of a bijective strong_hom_class can be realized as a first_order isomorphism.

Equations
@[protected, instance]
def first_order.language.strong_hom_class_empty {F : Type u_1} {M : out_param (Type u_2)} {N : Type u_3} [fun_like F M (λ (_x : M), N)] :
Equations
def function.empty_hom {M : Type w} {N : Type w'} (f : M → N) :

Makes a language.empty.hom out of any function.

Equations
@[simp]
theorem function.empty_hom_to_fun {M : Type w} {N : Type w'} (f : M → N) (ᾰ : M) :
(function.empty_hom f) = f ᾰ
def embedding.empty {M : Type w} {N : Type w'} (f : M N) :

Makes a language.empty.embedding out of any function.

Equations
@[simp]
theorem embedding.empty_to_embedding {M : Type w} {N : Type w'} (f : M N) :
def equiv.empty {M : Type w} {N : Type w'} (f : M N) :

Makes a language.empty.equiv out of any function.

Equations
@[simp]
theorem equiv.empty_to_equiv {M : Type w} {N : Type w'} (f : M N) :
@[simp]
theorem equiv.induced_Structure_rel_map {L : first_order.language} {M : Type u_3} {N : Type u_4} [L.Structure M] (e : M N) (n : ) (r : L.relations n) (x : fin n → N) :
def equiv.induced_Structure {L : first_order.language} {M : Type u_3} {N : Type u_4} [L.Structure M] (e : M N) :

A structure induced by a bijection.

Equations
@[simp]
theorem equiv.induced_Structure_fun_map {L : first_order.language} {M : Type u_3} {N : Type u_4} [L.Structure M] (e : M N) (n : ) (f : L.functions n) (x : fin n → N) :
@[simp]
theorem equiv.induced_Structure_equiv_to_equiv_apply {L : first_order.language} {M : Type u_3} {N : Type u_4} [L.Structure M] (e : M N) (ᾰ : M) :
@[simp]
theorem equiv.induced_Structure_equiv_to_equiv_symm_apply {L : first_order.language} {M : Type u_3} {N : Type u_4} [L.Structure M] (e : M N) (ᾰ : N) :
def equiv.induced_Structure_equiv {L : first_order.language} {M : Type u_3} {N : Type u_4} [L.Structure M] (e : M N) :
L.equiv M N

A bijection as a first-order isomorphism with the induced structure on the codomain.

Equations