eq_top_iff'

Mathlib.Algebra.Group.Submonoid.Operations

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

English

For a submonoid S of M, S = ⊤ if and only if every element of M belongs to S.

Русский

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

LaTeX

$$$ \text{eq_top_iff'} : S = \top \leftrightarrow \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