English
If a ∉ s, then the map X ↦ insert a X from 𝒫(s) to 𝒫(α) is injective.
Русский
Если a ∉ s, то отображение X ↦ X ∪ {a} из 𝒫(s) в 𝒫(α) инъективно.
LaTeX
$$$\\operatorname{InjOn}(insert\\ a, \\mathcal{P}(s))$ if $a \\notin s$$$
Lean4
theorem powerset_insert_injOn {s : Set α} {a : α} (h : a ∉ s) : Set.InjOn (insert a) (𝒫 s) := fun u u_mem v v_mem eq ↦
by
rw [Subset.antisymm_iff] at eq ⊢
rwa [Set.insert_subset_insert_iff <| Set.notMem_subset ((mem_powerset_iff _ _).mp v_mem) h,
Set.insert_subset_insert_iff <| Set.notMem_subset ((mem_powerset_iff _ _).mp u_mem) h] at eq