English
Characterization: for n : Finsupp (Option α) M, m : α →₀ M, i : M, we have n = (embDomain Embedding.some m).update none i iff n none = i and n.some = m.
Русский
Характеризация: для n : Finsupp (Option α) M, m : α →₀ M, i : M выполняется n = (embDomain Embedding.some m).update none i тогда и только тогда, когда n.none = i и n.some = m.
LaTeX
$$$ n = (embDomain Embedding.some m).update none i \iff (n none = i) \land (n. some = m) $$$
Lean4
theorem eq_option_embedding_update_none_iff [Zero M] {n : Option α →₀ M} {m : α →₀ M} {i : M} :
n = (embDomain Embedding.some m).update none i ↔ n none = i ∧ n.some = m :=
(optionEquiv.apply_eq_iff_eq_symm_apply (y := (_, _))).symm.trans Prod.ext_iff