mem_range_pred_of_not_isPredPrelimit

Mathlib.Order.SuccPred.Limit

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

← MathLib Explorer

English

If ¬IsPredPrelimit a, then a ∈ range(pred).

Русский

Если не IsPredPrelimit a, то a ∈ образ pred.

LaTeX

$$a \in range(pred)$$

Lean4

/-- See `not_isPredPrelimit_iff` for a version that states that `a` is a successor of a value other
than itself. -/
theorem mem_range_pred_of_not_isPredPrelimit (h : ¬IsPredPrelimit a) : a ∈ range (pred : α → α) :=
  by
  obtain ⟨b, hb⟩ := not_isPredPrelimit_iff.1 h
  exact ⟨b, hb.2⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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