one_notMem_iff

Mathlib.Algebra.Order.Monoid.Canonical.Defs

URI: https://scilib.ai/kg/mathlib#one_notMem_iff

English

If a < b in a canonically ordered monoid, there exists c > 1 with a·c = b.

Русский

Если a < b в канонически упорядоченном моноиде, существует c > 1 с a·c = b.

LaTeX

$$$ a < b \\rightarrow \\exists c > 1,\\; a \\cdot c = b $$$

Lean4

@[to_additive]
theorem one_notMem_iff [OrderBot α] {s : Set α} : 1 ∉ s ↔ ∀ x ∈ s, 1 < x :=
  bot_eq_one (α := α) ▸ bot_notMem_iff

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

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

Разделы

Аффилиация

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