English
For every f in the codomain of the keys-Lookup equivalence, the keys of the Finmap obtained by applying the inverse of the equivalence are exactly the first component of f.
Русский
Для каждого элемента f в кодоморфизме эквивалентности keysLookupEquiv, ключи отображения, полученного применением обратной карты, равны первому компоненту f.
LaTeX
$$$ \forall f,\ (\mathrm{keysLookupEquiv}.\mathrm{symm}\, f).\text{keys} = f.\text{val}.\text{fst}$$$
Lean4
@[simp]
theorem keysLookupEquiv_symm_apply_keys :
∀ f : { f : Finset α × (∀ a, Option (β a)) // ∀ i, (f.2 i).isSome ↔ i ∈ f.1 },
(keysLookupEquiv.symm f).keys = f.1.1 :=
keysLookupEquiv.surjective.forall.2 fun _ => by simp only [Equiv.symm_apply_apply, keysLookupEquiv_apply_coe_fst]
