eq_bot_of_subsingleton

Mathlib.Algebra.Group.Submonoid.Operations

URI: https://scilib.ai/kg/mathlib#Submonoid.eq_bot_of_subsingleton

← MathLib Explorer

English

Let S be a submonoid with Subsingleton (Subtype ...) structure; then S = ⊥.

Русский

Пусть S — подмонойд с подмножеством Subsingleton; тогда S = ⊥.

LaTeX

$$$ \text{eq\_bot\_of\_subsingleton} (S) $$$

Lean4

@[to_additive]
theorem eq_bot_of_subsingleton [Subsingleton S] : S = ⊥ :=
  by
  rw [eq_bot_iff_forall]
  intro y hy
  simpa using congr_arg ((↑) : S → M) <| Subsingleton.elim (⟨y, hy⟩ : S) 1

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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