kstar_eq_one

Mathlib.Algebra.Order.Kleene

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

← MathLib Explorer

English

a* = 1 iff a ≤ 1.

Русский

a^* = 1 тогда как только a ≤ 1, и наоборот.

LaTeX

$$$a^* = 1 \iff a \le 1$$$

Lean4

@[simp]
theorem kstar_eq_one : a∗ = 1 ↔ a ≤ 1 :=
  ⟨le_kstar.trans_eq, fun h ↦ one_le_kstar.antisymm' <| kstar_le_of_mul_le_left le_rfl <| by rwa [one_mul]⟩

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

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

Разделы

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

Аффилиация

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