notMem_one

Mathlib.Algebra.FreeMonoid.Basic

URI: https://scilib.ai/kg/mathlib#FreeMonoid.notMem_one

English

For any m in α, m is in of n iff m = n.

Русский

Для любого m ∈ α верно: m ∈ of n тогда и только тогда, когда m = n.

LaTeX

$$$\\\\forall {n : α}, \\\\; m \\\\in of n \\\\iff \\\\; m = n$$$

Lean4

@[to_additive]
theorem notMem_one : m ∉ (1 : FreeMonoid α) :=
  List.not_mem_nil

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

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

Разделы

Аффилиация

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