mk_left_injective — Mathlib

English

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

Русский

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

LaTeX

$$$\\\\forall a_1,a_2 \\\\in \\\\alpha, (a_1,b)=(a_2,b) \\\\iff a_1=a_2.$$$

Lean4

theorem mk_left_injective {α β : Type*} (b : β) : (fun a ↦ mk a b : α → α × β).Injective :=
  by
  intro b₁ b₂ h
  simpa only [and_true, eq_self_iff_true, mk_inj] using h

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