insert_union_comm — Mathlib

English

Inserting a into s and then union with t equals s union inserting a into t: insert a s ∪ t = s ∪ insert a t.

Русский

Вставка a в s и объединение с t эквивалентны объединению s с вставкой a в t.

LaTeX

$$insert_union_comm (s t : Finset α) (a : α) : insert a s ∪ t = s ∪ insert a t$$

Lean4

theorem insert_union_comm (s t : Finset α) (a : α) : insert a s ∪ t = s ∪ insert a t := by
  rw [insert_union, union_insert]

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