not_isSuccPrelimit_iff — Mathlib

English

The negation of IsSuccPrelimit a is equivalent to the existence of a witness b that is not maximal and satisfies succ b = a.

Русский

Отрицание IsSuccPrelimit(a) эквивалентно существованию элемента b, который не является максимальным и удовлетворяет succ b = a.

LaTeX

$$$\neg IsSuccPrelimit(a) \iff \exists b, \neg IsMax(b) \land succ(b) = a$$$

Lean4

theorem not_isSuccPrelimit_iff : ¬IsSuccPrelimit a ↔ ∃ b, ¬IsMax b ∧ succ b = a :=
  by
  rw [not_isSuccPrelimit_iff_exists_covBy]
  refine exists_congr fun b => ⟨fun hba => ⟨hba.lt.not_isMax, (CovBy.succ_eq hba)⟩, ?_⟩
  rintro ⟨h, rfl⟩
  exact covBy_succ_of_not_isMax h

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