iSup_Iio_eq_self_iff_isSuccPrelimit

English

For a ConditionallyCompleteLinearOrderBot with a well-founded order, iSup over Iio x equals x if and only if IsPredPrelimit x.

Русский

Для условно полноупорядоченного порядка с нижним элементом, iSup по Iio x равен x тогда и только тогда, когда IsPredPrelimit x.

LaTeX

$$$ iSup Iio x = x \\iff IsPredPrelimit x $$$

Lean4

theorem iSup_Iio_eq_self_iff_isSuccPrelimit : ⨆ a : Iio x, a.1 = x ↔ IsSuccPrelimit x := by
  rw [← sSup_eq_iSup', sSup_Iio_eq_self_iff_isSuccPrelimit]

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