English
Creates a PEquiv that acts as the identity on a given set s and maps outside to none, with the inverse defined accordingly.
Русский
Строится PEquiv, который действует как тождественный на множество s и за пределами него отображает в none, с соответствующим обратным отображением.
LaTeX
$$$$ \\mathrm{ofSet}(s) : \\alpha \\to \\alpha \\quad\\text{с} \\quad \\text{toFun}(a)=\\begin{cases} \\text{some } a & a\\in s \\\\ none & \\text{иначе} \\end{cases}, \\ \\text{invFun}(a)=\\begin{cases} \\text{some } a & a\\in s \\\\ none & \\text{иначе} \\end{cases}. $$$$
Lean4
/-- Creates a `PEquiv` that is the identity on `s`, and `none` outside of it. -/
def ofSet (s : Set α) [DecidablePred (· ∈ s)] : α ≃. α
where
toFun a := if a ∈ s then some a else none
invFun a := if a ∈ s then some a else none
inv a
b := by
split_ifs with hb ha ha
· simp [eq_comm]
· simp [ne_of_mem_of_not_mem hb ha]
· simp [ne_of_mem_of_not_mem ha hb]
· simp
