isSuccLimit_toDual_iff

Mathlib.Order.SuccPred.Limit

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

English

If b is a predecessor-prelimit, then b ≤ succ(a) iff b ≤ a.

Русский

Если b — пред-предлимит, то b ≤ succ(a) эквивално b ≤ a.

LaTeX

$$$\IsSuccPrelimit(b) \Rightarrow (b \le \text{succ}(a) \iff b \le a)$$$

Lean4

@[simp]
theorem isSuccLimit_toDual_iff : IsSuccLimit (toDual a) ↔ IsPredLimit a := by simp [IsSuccLimit, IsPredLimit]

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

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

Разделы

Аффилиация

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