inv_coe_set

Mathlib.Algebra.Group.Subgroup.Pointwise

URI: https://scilib.ai/kg/mathlib#inv_coe_set

← MathLib Explorer

English

The inverse of the underlying set of a subgroup equals the subgroup itself.

Русский

Обратное множества подгруппы совпадает с самой подгруппой.

LaTeX

$$(H : Set G)^{-1} = H$$

Lean4

@[to_additive (attr := simp, norm_cast)]
theorem inv_coe_set [InvolutiveInv G] [SetLike S G] [InvMemClass S G] {H : S} : (H : Set G)⁻¹ = H :=
  Set.ext fun _ => inv_mem_iff

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru