mem_lists_iff_coe_eq — Mathlib

English

The multiset of lists of nil equals the singleton set containing the empty list.

Русский

Мультимножество списков пустого цикла содержит только пустой список.

LaTeX

$$$lists(\Cycle.nil) = {([] : List \alpha)}$$$

Lean4

@[simp]
theorem mem_lists_iff_coe_eq {s : Cycle α} {l : List α} : l ∈ s.lists ↔ (l : Cycle α) = s :=
  Quotient.inductionOn' s fun l => by
    rw [lists, Quotient.liftOn'_mk'']
    simp

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