mk_right_injective — Mathlib

English

For a fixed a ∈ α, the map b ↦ (a,b) : β → α × β is injective.

Русский

Для фиксированного a ∈ α отображение b ↦ (a,b) : β → α × β инъективно.

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_injective {α β : Type*} (a : α) : (mk a : β → α × β).Injective :=
  by
  intro b₁ b₂ h
  simpa only [true_and, Prod.mk_inj, eq_self_iff_true] using h

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