apply_eq_iff_eq

Mathlib.Logic.Embedding.Basic

URI: https://scilib.ai/kg/mathlib#Function.Embedding.apply_eq_iff_eq

English

Let f: α ↪ β and x,y ∈ α. Then f x = f y ⇔ x = y.

Русский

Пусть f: α ↪ β и x,y ∈ α. Тогда f x = f y ⇔ x = y.

LaTeX

$$$f : \\alpha \\hookrightarrow \\beta\\quad\\forall x,y\\in\\alpha,\\ f(x)=f(y) \\iff x=y$$$

Lean4

theorem apply_eq_iff_eq {α β} (f : α ↪ β) (x y : α) : f x = f y ↔ x = y :=
  EmbeddingLike.apply_eq_iff_eq f

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

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

Разделы

Аффилиация

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