mem_range_succ_of_not_isSuccPrelimit

English

If a is not a succ-prelimit, then a is in the range of the successor map.

Русский

Если a не является succ-предпредельным, то существует b such that succ(b) = a.

LaTeX

$$$\neg IsSuccPrelimit(a) \Rightarrow a \in \operatorname{range}(\mathrm{succ})$$$

Lean4

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

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