Theorems · Definition · combinatorics
Finmap.keys
{α : Type u} → {β : α → Type v} → Finmap β → Finset αThe set of keys of a finite map.
- Defined in
- Mathlib.Data.Finmap
- Cited by
- 12 results in Mathlib
- Foundations
- Depth 27 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Finsetstatement · cited by 13,712
- Finmapstatement and proof · cited by 81
- Finmap.entriesproof · cited by 14
- Multiset.keysproof · cited by 9
Cited by13
Results whose statement or proof uses this declaration.
- Finmap.keysLookupEquivproof · cited by 4
- Finmap.keysLookupEquiv_apply_coe_fststatement · cited by 1
- Finmap.keys_erase_toFinsetstatement and proof · cited by 1
- Finmap.sigma_keys_lookupstatement and proof · cited by 0
- Finmap.keysLookupEquiv_symm_apply_keysstatement and proof · cited by 0
- Finmap.mem_keysstatement · cited by 0
- Finmap.keys_emptystatement · cited by 0
- Finmap.keys_erasestatement and proof · cited by 0
- Finmap.keys_extstatement · cited by 0
- Finmap.keys_replacestatement and proof · cited by 0
- Finmap.keys_singletonstatement · cited by 0
- Finmap.keys_unionstatement · cited by 0