ext

Mathlib.ModelTheory.ElementaryMaps

URI: https://scilib.ai/kg/mathlib#FirstOrder.Language.ElementaryEmbedding.ext

English

If two L-elementary embeddings f and g from M to N agree on every element of M, then f = g.

Русский

Если два элементарных вложения L: M → N согласны на каждом элементе M, то они равны.

LaTeX

$$$\forall f,g: M \hookrightarrow_L N,\ (\forall x \in M:\ f(x)=g(x)) \Rightarrow f=g$$$

Lean4

@[ext]
theorem ext ⦃f g : M ↪ₑ[L] N⦄ (h : ∀ x, f x = g x) : f = g :=
  DFunLike.ext f g h

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru