English
For every f and every a, the lookup value of the Finmap obtained by the inverse of the equivalence equals the second component of f applied to a.
Русский
Для каждого f и каждого a значение поиска в Finmap, полученном через обратное отображение, равно второй компоненте f, применённой к a.
LaTeX
$$$ \forall f:\{ f : Finset\alpha \times (\forall a, \mathrm{Option}(\beta a)) // \forall i, (f.2 i).isSome \iff i \in f.1 \},\forall a,\ \operatorname{lookup}(a, \mathrm{keysLookupEquiv}^{-1}(f)) = f.1.2(a). $$$
Lean4
@[simp]
theorem keysLookupEquiv_symm_apply_lookup :
∀ (f : { f : Finset α × (∀ a, Option (β a)) // ∀ i, (f.2 i).isSome ↔ i ∈ f.1 }) a,
(keysLookupEquiv.symm f).lookup a = f.1.2 a :=
keysLookupEquiv.surjective.forall.2 fun _ _ => by simp only [Equiv.symm_apply_apply, keysLookupEquiv_apply_coe_snd]
