English
There is a natural equivalence between Finmap β and the set of pairs (K, L) with K a Finset α and L : α → Option(β a) such that for all i, L(i) isSome iff i ∈ K.
Русский
Существует естественное эквивалентное отображение между Finmap β и множеством пар (K, L), где K — конечный набор элементов α, а L: α → Option(β a) таково, что для каждого i выполняется L(i) есть тогда и только тогда, когда i ∈ K.
LaTeX
$$$ Finmap\, \beta \simeq \{ f : Finset\, \alpha \times (\forall a, \mathrm{Option}(\beta(a))) \;\big|\; \forall i, (f.2 i).\mathrm{isSome} \iff i \in f.1 \} $$$
Lean4
/-- An equivalence between `Finmap β` and pairs `(keys : Finset α, lookup : ∀ a, Option (β a))` such
that `(lookup a).isSome ↔ a ∈ keys`. -/
@[simps apply_coe_fst apply_coe_snd]
def keysLookupEquiv : Finmap β ≃ { f : Finset α × (∀ a, Option (β a)) // ∀ i, (f.2 i).isSome ↔ i ∈ f.1 }
where
toFun s := ⟨(s.keys, fun i => s.lookup i), fun _ => lookup_isSome⟩
invFun
f :=
mk (f.1.1.sigma fun i => (f.1.2 i).toFinset).val <|
by
refine Multiset.nodup_keys.1 ((Finset.nodup _).map_on ?_)
simp only [Finset.mem_val, Finset.mem_sigma, Option.mem_toFinset, Option.mem_def]
rintro ⟨i, x⟩ ⟨_, hx⟩ ⟨j, y⟩ ⟨_, hy⟩ (rfl : i = j)
simpa using hx.symm.trans hy
left_inv f := ext <| by simp
right_inv := fun ⟨(s, f), hf⟩ => by
dsimp only at hf
ext
· simp [keys, Multiset.keys, ← hf, Option.isSome_iff_exists]
· simp +contextual [lookup_eq_some_iff, ← hf]
