set_of_mem_cons — Mathlib

English

The set of elements of a :: l equals the insertion into the set of elements of l by a; i.e., {x | x ∈ a :: l} = insert a {x | x ∈ l}.

Русский

Множество элементов a :: l равно вставке элемента a в множество элементов l: {x | x ∈ a :: l} = insert a {x | x ∈ l}.

LaTeX

$$setOf (fun x => x ∈ List.cons a l) = Set.insert a (setOf (fun x => x ∈ l))$$

Lean4

theorem set_of_mem_cons (l : List α) (a : α) : {x | x ∈ a :: l} = insert a {x | x ∈ l} :=
  Set.ext fun _ => mem_cons

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