toSubgroup_injective — Mathlib

English

The map sending an open subgroup U to the corresponding Subgroup U.toSubgroup is injective.

Русский

Отображение открытой подгруппы U в соответствующую подгруппу U.toSubgroup инъективно.

LaTeX

$$$\forall U,V \in \mathrm{OpenSubgroup}(G),\ U.toSubgroup = V.toSubgroup \Rightarrow U = V$$$

Lean4

@[to_additive]
theorem toSubgroup_injective : Injective ((↑) : OpenSubgroup G → Subgroup G)
  | ⟨_, _⟩, ⟨_, _⟩, rfl => rfl

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