coe_nonempty

Mathlib.Algebra.Group.Subgroup.Defs

URI: https://scilib.ai/kg/mathlib#Subgroup.coe_nonempty

English

The underlying set of a subgroup is nonempty.

Русский

Носитель подгруппы непуст.\.

LaTeX

$$$(s : Set G).Nonempty$$

Lean4

@[to_additive (attr := simp)]
theorem coe_nonempty (s : Subgroup G) : (s : Set G).Nonempty :=
  ⟨1, one_mem _⟩

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

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

Разделы

Аффилиация

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