insert_erase_invOn — Mathlib

English

The pair of operations insert a and s ↦ s \\ {a} form an inverse on the two complementary domains: {s | a ∈ s} and {s | a ∉ s}.

Русский

Пара операций вставки элемента a и удаления {a} образуют взаимно обратные на двух взаимно дополняющих множеств: {s | a ∈ s} и {s | a ∉ s}.

LaTeX

$$$ \\text{InvOn}(\\text{insert } a,\\, s \\mapsto s \\setminus \\{a\\},\\, \\{s \\mid a \\in s\\},\\, \\{s \\mid a \\notin s\\}) $$$

Lean4

theorem insert_erase_invOn : InvOn (insert a) (fun s ↦ s \ { a }) {s : Set α | a ∈ s} {s : Set α | a ∉ s} :=
  ⟨fun _s ha ↦ insert_diff_self_of_mem ha, fun _s ↦ insert_diff_self_of_notMem⟩

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