sSup_Iio_eq_self_iff_isSuccPrelimit

English

For any α with a bottom, sSup(Iio x) = x if and only if IsSuccPrelimit x.

Русский

Для любого α с нижним элементом sSup(Iio x) = x тогда и только тогда, когда IsSuccPrelimit x.

LaTeX

$$$ sSup(Iio x) = x \\iff IsSuccPrelimit x $$$

Lean4

theorem sSup_Iio_eq_self_iff_isSuccPrelimit : sSup (Iio x) = x ↔ IsSuccPrelimit x :=
  by
  refine ⟨fun h ↦ ?_, IsSuccPrelimit.sSup_Iio⟩
  by_contra hx
  rw [← h] at hx
  simpa [h] using csSup_mem_of_not_isSuccPrelimit' bddAbove_Iio hx

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