insertNone_eraseNone — Mathlib

English

Applying eraseNone after insertNone recovers the original Finset: eraseNone(insertNone(s)) = s.

Русский

Применение eraseNone после insertNone восстанавливает исходное Finset: eraseNone(insertNone(s)) = s.

LaTeX

$$$\\text{eraseNone}(\\text{insertNone}(s)) = s$$$

Lean4

@[simp]
theorem insertNone_eraseNone [DecidableEq (Option α)] (s : Finset (Option α)) :
    insertNone (eraseNone s) = insert none s := by ext (_ | x) <;> simp

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