sdiff_insert_insert_of_mem_of_notMem

English

Let S, T be finite subsets and x ∈ A with x ∈ S and x ∉ T. Then S \\ T = insert x (S \\ (T ∪ {x})).

Русский

Пусть S, T — конечные подмножества и x ∈ A так, что x ∈ S и x ∉ T. Тогда S \\ T = вставка x (S \\ (T ∪ {x})).

LaTeX

$$$S \\setminus T = \\operatorname{insert}(x, S \\setminus (T \\cup \\{x\\}))$$$

Lean4

theorem sdiff_insert_insert_of_mem_of_notMem {s t : Finset α} {x : α} (hxs : x ∈ s) (hxt : x ∉ t) :
    insert x (s \ insert x t) = s \ t := by grind

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