Theorems · Theorem · combinatorics
Finmap.keys_union
∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] {s₁ s₂ : Finmap β}, (s₁ ∪ s₂).keys = s₁.keys ∪ s₂.keys- Defined in
- Mathlib.Data.Finmap
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 56 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- DecidableEq
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites15
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Finsetstatement · cited by 13,712
- Finset.extproof · cited by 565
- Multiset.ofListproof · cited by 290
- AListproof · cited by 122
- Finmapstatement and proof · cited by 81
- List.keysproof · cited by 46
- AList.entriesproof · cited by 44
- AList.toFinmapproof · cited by 33
- List.kunionproof · cited by 18
- Finmap.entriesproof · cited by 14
- Finmap.keysstatement · cited by 12
- Finmap.induction_on₂proof · cited by 10
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.