keys_union — Mathlib

English

For Finmap β, the set of keys of the union equals the union of the keys: (s1 ∪ s2).keys = s1.keys ∪ s2.keys.

Русский

Для Finmap β множество ключей объединения равно объединению множеств ключей исходных множеств.

LaTeX

$$$ (s_1 \cup s_2).keys = s_1.keys \cup s_2.keys $$$

Lean4

theorem keys_union {s₁ s₂ : Finmap β} : (s₁ ∪ s₂).keys = s₁.keys ∪ s₂.keys :=
  induction_on₂ s₁ s₂ fun s₁ s₂ => Finset.ext <| by simp [keys]

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