setOf_mem_list_eq_singleton_of_nodup

English

Let l be a nodup list in α and a ∈ α. Then { x | x ∈ l } = { a } if and only if l = [ a ].

Русский

Пусть l — список α без повторов. Тогда { x | x ∈ l } = { a } тогда l = [ a ].

LaTeX

$$$\mathrm{Nodup}(l) \Rightarrow \left( \{ x \mid x \in l \} = \{ a \} \iff l = [a] \right)$$$

Lean4

theorem setOf_mem_list_eq_singleton_of_nodup {l : List α} (H : l.Nodup) {a : α} : {x | x ∈ l} = { a } ↔ l = [a] :=
  by
  constructor
  · rw [setOf_mem_list_eq_replicate]
    rintro ⟨n, hn, rfl⟩
    simp only [List.nodup_replicate] at H
    simp [show n = 1 by cutsat]
  · rintro rfl
    simp
      -- while `simp` is capable of proving this, it is not capable of turning the LHS into the RHS.

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