instNontrivialSubtypeMemTop

Mathlib.Algebra.Group.Subgroup.Lattice

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

English

If G is nontrivial, then the subtype of the top subgroup is nontrivial.

Русский

Если G ненулевой, то подсистема верхней подпгруппы ненулевая.

LaTeX

$$Nontrivial(Subtype (fun x => x ∈ ⊤))$$

Lean4

@[to_additive]
instance [Nontrivial G] : Nontrivial (⊤ : Subgroup G) :=
  by
  rw [nontrivial_iff_ne_bot]
  exact top_ne_bot

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

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

Разделы

Аффилиация

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