length_of_sublistsLen — Mathlib

English

If l' is an element of sublistsLen n l then its length equals n.

Русский

Если l' является элементом sublistsLen n l, то |l'| = n.

LaTeX

$$$\\forall {\\alpha} {n} {l} {l'}:\\ l' \\in \\operatorname{sublistsLen}(n, l) \\Rightarrow \\operatorname{length}(l') = n$$$

Lean4

theorem length_of_sublistsLen : ∀ {n} {l l' : List α}, l' ∈ sublistsLen n l → length l' = n
  | 0, l, l', h => by simp_all
  | n + 1, a :: l, l', h => by
    rw [sublistsLen_succ_cons, mem_append, mem_map] at h
    rcases h with (h | ⟨l', h, rfl⟩)
    · exact length_of_sublistsLen h
    · exact congr_arg (· + 1) (length_of_sublistsLen h)

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