cons_inj — Mathlib

English

Equality of cons implies equality of heads and tails: cons x0 x = cons y0 y iff x0 = y0 and x = y.

Русский

Равенство cons подразумевает равенство голов и хвостов: cons x0 x = cons y0 y тогда и только тогда, когда x0 = y0 и x = y.

LaTeX

$$$(\\\\mathrm{cons}(x_0,x) = \\\\mathrm{cons}(y_0,y)) \\iff (x_0 = y_0 \\land x = y)$$$

Lean4

@[simp]
theorem cons_inj {x₀ y₀ : α 0} {x y : ∀ i : Fin n, α i.succ} : cons x₀ x = cons y₀ y ↔ x₀ = y₀ ∧ x = y :=
  cons_injective2.eq_iff

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