ext

Mathlib.ModelTheory.Basic

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

English

If two L-embeddings agree on all elements of M, then they are equal as embeddings.

Русский

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

LaTeX

$$$\\forall x: 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 :=
  coe_injective (funext h)

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

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

Разделы

Аффилиация

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