length_eq — Mathlib

English

If Forall₂ R l1 l2 holds, then the lengths of l1 and l2 are equal.

Русский

Если Forall₂ R l1 l2 выполняется, тогда длины списков l1 и l2 равны.

LaTeX

$$$ \mathrm{Forall₂}\ R\ l_1\ l_2\ \Rightarrow\ \mathrm{length}\ l_1 = \mathrm{length}\ l_2 $$$

Lean4

theorem length_eq : ∀ {l₁ l₂}, Forall₂ R l₁ l₂ → length l₁ = length l₂
  | _, _, Forall₂.nil => rfl
  | _, _, Forall₂.cons _ h₂ => congr_arg succ (Forall₂.length_eq h₂)

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