inj_iff — Mathlib

English

Two PSigma.mks ⟨a1,b1⟩ and ⟨a2,b2⟩ are equal iff a1=a2 and b1 is HEq to b2.

Русский

Два PSigma.mk ⟨a1,b1⟩ и ⟨a2,b2⟩ равны тогда и только тогда, когда a1=a2 и b1 имеет гетерогенную эквивалентность с b2.

LaTeX

$$$@PSigma.mk \\ α \\ β a_1 b_1 = @PSigma.mk α β a_2 b_2 \\iff a_1 = a_2 \\land b_1 \\;\\mathrm{HEq} \\; b_2$$$

Lean4

theorem inj_iff {a₁ a₂ : α} {b₁ : β a₁} {b₂ : β a₂} : @PSigma.mk α β a₁ b₁ = @PSigma.mk α β a₂ b₂ ↔ a₁ = a₂ ∧ b₁ ≍ b₂ :=
  (Iff.intro PSigma.mk.inj) fun ⟨h₁, h₂⟩ ↦
    match a₁, a₂, b₁, b₂, h₁, h₂ with
    | _, _, _, _, Eq.refl _, HEq.refl _ => rfl

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