ofFixingSubgroupEmpty_equivariantMap_bijective

English

The map associated to the empty set is bijective:

Русский

Отображение, связанное с пустым множеством, является биекции.

LaTeX

$$$\text{Bijective}\bigl(ofFixingSubgroup\_equivariantMap\ M\ (\varnothing)\bigr).$$$

Lean4

@[to_additive]
theorem ofFixingSubgroupEmpty_equivariantMap_bijective : Bijective (ofFixingSubgroup_equivariantMap M (∅ : Set α)) :=
  by
  refine ⟨ofFixingSubgroup_equivariantMap_injective, fun x ↦ ?_⟩
  exact ⟨⟨x, (mem_ofFixingSubgroup_iff M).mp (Set.notMem_empty x)⟩, rfl⟩

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