mk_inj — Mathlib

English

Let a1,a2 ∈ α and b1,b2 ∈ β. Then (a1,b1) = (a2,b2) if and only if a1 = a2 and b1 = b2.

Русский

Пусть a1,a2 ∈ α и b1,b2 ∈ β. Тогда (a1,b1) = (a2,b2) тогда и только тогда, когда a1 = a2 и b1 = b2.

LaTeX

$$$\\\\forall a_1,a_2 \\\\in \\\\alpha \\\\forall b_1,b_2 \\\\in \\\\beta, (a_1,b_1)=(a_2,b_2) \\\\iff (a_1=a_2) \\\\land (b_1=b_2).$$$

Lean4

theorem mk_inj {a₁ a₂ : α} {b₁ b₂ : β} : (a₁, b₁) = (a₂, b₂) ↔ a₁ = a₂ ∧ b₁ = b₂ := by simp

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