eq_top_iff'

Mathlib.Algebra.Group.Subgroup.Lattice

URI: https://scilib.ai/kg/mathlib#Subgroup.eq_top_iff'

English

For a subgroup H of G, H = ⊤ iff every element of G lies in H.

Русский

Для подгруппы H группы G верно: H = ⊤ тогда и только тогда, когда каждый элемент G принадлежит H.

LaTeX

$$$H = \top \iff \forall x: G, x \in H$$$

Lean4

@[to_additive]
theorem eq_top_iff' : H = ⊤ ↔ ∀ x : G, x ∈ H :=
  eq_top_iff.trans ⟨fun h m => h <| mem_top m, fun h m _ => h m⟩

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

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

Разделы

Аффилиация

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