eq_option_embedding_update_none_iff

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

Похожие утверждения