eq_top_iff'

Mathlib.Algebra.Group.Subsemigroup.Operations

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

English

Let S be a subsemigroup of M. Then S = ⊤ if and only if every element of M lies in S.

Русский

Пусть S — подполугруппа M. Тогда S = ⊤ тогда и только тогда, когда каждый элемент M принадлежит S.

LaTeX

$$$S = \top \iff \forall x : M, x \in S$$$

Lean4

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

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

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

Разделы

Аффилиация

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