Theorems · Definition
List.keys
{α : Type u} → {β : α → Type v} → List (Sigma β) → List αList of keys from a list of key-value pairs
- Defined in
- Mathlib.Data.List.Sigma
- Cited by
- 46 results in Mathlib
- Foundations
- Depth 7 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites0
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
Nothing in Mathlib beyond the foundations.
Cited by49
Results whose statement or proof uses this declaration.
- List.NodupKeysproof · cited by 53
- AList.keysproof · cited by 13
- AList.lookupFinsuppproof · cited by 9
- List.kerase_of_notMem_keysstatement and proof · cited by 6
- List.keys_kerasestatement · cited by 4
- List.mem_dlookup_kunionstatement and proof · cited by 4
- List.nodupKeys_consstatement · cited by 4
- List.dlookup_isSomestatement and proof · cited by 3
- List.keys_kreplacestatement · cited by 2
- List.notMem_keys_kerasestatement and proof · cited by 2
- List.notMem_keys_of_nodupKeys_consstatement · cited by 2
- List.exists_of_kerasestatement and proof · cited by 2