ext — Mathlib

English

Two lists have equal toFinsets iff they have the same membership for all elements.

Русский

Две последовательности имеют одинаковые toFinset тогда и только тогда, когда для каждого элемента выполняется равенство принадлежности.

LaTeX

$$$\\forall {l l' : \\mathsf{List}\\,\\alpha},\\; (\\forall x, x \\in l \\iff x \\in l') \\Rightarrow l.toFinset = l'.toFinset$$$

Lean4

theorem ext : (∀ x, x ∈ l ↔ x ∈ l') → l.toFinset = l'.toFinset :=
  toFinset.ext_iff.mpr

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