length_injective_iff — Mathlib

English

Injective length is equivalent to Subsingleton α; length is injective iff α is subsingleton.

Русский

Инъективность длины эквивалентна тому, что α — подсинглот; длина инъективна тогда и только тогда, когда α — подсинглтон.

LaTeX

$$Injective( length ) ↔ Subsingleton α$$

Lean4

@[simp]
theorem length_injective_iff : Injective (List.length : List α → ℕ) ↔ Subsingleton α :=
  by
  constructor
  · intro h; refine ⟨fun x y => ?_⟩; (suffices [x] = [y] by simpa using this); apply h; rfl
  · intro hα l1 l2 hl
    induction l1 generalizing l2 <;> cases l2
    · rfl
    · cases hl
    · cases hl
    ·
      next ih _ _ =>
        congr
        · subsingleton
        · apply ih; simpa using hl

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