isPredPrelimit_iff

Mathlib.Order.SuccPred.Limit

URI: https://scilib.ai/kg/mathlib#Order.isPredPrelimit_iff

English

In this setting, a is a predecessor-prelimit if and only if a is the maximum element.

Русский

В данной постановке a эквивалентно является максимумом тогда и только тогда, когда оно предпредельное.

LaTeX

$$$IsPredPrelimit\\ a \\iff IsMax\\ a$$$

Lean4

@[simp]
theorem isPredPrelimit_iff : IsPredPrelimit a ↔ IsMax a :=
  ⟨IsPredPrelimit.isMax, IsMax.isPredPrelimit⟩

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

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

Разделы

Аффилиация

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