English
The pair (insert a) followed by (erase a) is an inverse on the set of all Finsets containing a; conversely, (erase a) then (insert a) is inverse on the set of Finsets not containing a.
Русский
Операции вставки элемента a и удаления элемента a образуют взаимно обратные на множествах Finset, содержащих a, и на множествах, не содержащих a.
LaTeX
$$$$ \text{Insert}^{-1} \text{Erase} = \text{Id} \text{ on } \{s : Finset \ α \mid a \in s\}, \quad \text{Erase}^{-1} \text{Insert} = \text{Id} \text{ on } \{s : Finset \ α \mid a \notin s\}. $$$$
Lean4
theorem insert_erase_invOn : Set.InvOn (insert a) (fun s ↦ erase s a) {s : Finset α | a ∈ s} {s : Finset α | a ∉ s} :=
⟨fun _s ↦ insert_erase, fun _s ↦ erase_insert⟩
