powerset_insert_injOn — Mathlib

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

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