Theorems · Theorem · combinatorics

Finmap.sigma_keys_lookup

∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] (s : Finmap β),
  (s.keys.sigma fun i => (Finmap.lookup i s).toFinset) = { val := s.entries, nodup := ⋯ }

Defined in

Mathlib.Data.Finmap

Cited by

0 results in Mathlib

Foundations

Depth 65 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

DecidableEq