mk_right_inj

Mathlib.Data.Prod.Basic

URI: https://scilib.ai/kg/mathlib#Prod.mk_right_inj

English

For a fixed a ∈ α, the equality (a,b1) = (a,b2) holds iff b1 = b2.

Русский

Для фиксированного a ∈ α, равенство (a,b1) = (a,b2) эквивалентно b1 = b2.

LaTeX

$$$\\\\forall a \\\\in \\\\alpha, \\\\forall b_1,b_2 \\\\in \\\\beta, (a,b_1)=(a,b_2) \\\\iff b_1=b_2.$$$

Lean4

theorem mk_right_inj {a : α} {b₁ b₂ : β} : (a, b₁) = (a, b₂) ↔ b₁ = b₂ :=
  (mk_right_injective _).eq_iff

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

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

Разделы

Аффилиация

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