isPredPrelimit_toDual_iff — Mathlib

English

The succ-prelimit notion on an order corresponds to the pred-prelimit notion on the dual order.

Русский

Предел предшественника в одном порядке соответствует пределу предшественника в двойственном порядке.

LaTeX

$$$IsSuccPrelimit(toDual(a)) \iff IsPredPrelimit(a)$$$

Lean4

@[simp]
theorem isPredPrelimit_toDual_iff : IsPredPrelimit (toDual a) ↔ IsSuccPrelimit a := by
  simp [IsSuccPrelimit, IsPredPrelimit]

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