length_pos_of_mem_splitWrtComposition

English

If a sublist l' appears as an element of the split of l along c, then l' has positive length.

Русский

Если подсписок l' является элементом разбиения l по c, то длина l' положительна.

LaTeX

$$$\forall l',\; l' \in l.splitWrtComposition c \Rightarrow 0 < |l'|$$$

Lean4

theorem length_pos_of_mem_splitWrtComposition {l l' : List α} {c : Composition l.length}
    (h : l' ∈ l.splitWrtComposition c) : 0 < length l' :=
  by
  have : l'.length ∈ (l.splitWrtComposition c).map List.length := List.mem_map_of_mem h
  rw [map_length_splitWrtComposition] at this
  exact c.blocks_pos this

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