JointEmbedding — Mathlib

English

A class K has the joint embedding property when for any M,N in K, there exists a structure Q in K into which both M and N embed.

Русский

Класс K обладает свойством совместной вложимости: для любых M,N ∈ K существуют Q ∈ K и вложения M → Q, N → Q.

LaTeX

$$$\text{JointEmbedding}(K) \;:=\; \forall M,N \in K,\; \exists Q \in K,\; \exists (M\to Q), (N\to Q) . $$$

Lean4

/-- A class `K` has the joint embedding property when for every `M`, `N` in `K`, there is another
  structure in `K` into which both `M` and `N` embed. -/
def JointEmbedding : Prop :=
  DirectedOn (fun M N : Bundled.{w} L.Structure => Nonempty (M ↪[L] N)) K

Похожие утверждения