length_destutter_le_length_destutter_cons

English

For a suitable equivalence, the lengths satisfy monotonicity: len(destutter_R l) ≤ len(destutter_R (a :: l)).

Русский

При надлежащей эквивалентности длины удовлетворяют монотонности: длина destutter_R(l) ≤ длина destutter_R(a :: l).

LaTeX

$$$\\forall l,\\ \\text{len}(\\mathrm{destutter}_R(l)) \\le \\text{len}(\\mathrm{destutter}_R(a::l)).$$$

Lean4

/-- `List.destutter` on a relation like ≠, whose negation is an equivalence, has length
monotone under List.cons -/
theorem length_destutter_le_length_destutter_cons [IsEquiv α Rᶜ] :
    ∀ {l : List α}, (l.destutter R).length ≤ ((a :: l).destutter R).length
  | [] => by simp [destutter]
  | b :: l => le_length_destutter'_cons

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