not_isPredPrelimit_iff' — Mathlib

English

Not being a predecessor-prelimit is equivalent to a being in the range of pred.

Русский

Не быть предшественник-предпредельным эквивалентно тому, что a принадлежит образу pred.

LaTeX

$$$\\neg IsPredPrelimit\\ a \\iff a \\in \\operatorname{range}(\\operatorname{pred})$$$

Lean4

theorem not_isPredPrelimit_iff' : ¬IsPredPrelimit a ↔ a ∈ range (pred : α → α) := by
  simp_rw [isPredPrelimit_iff_pred_ne, not_forall, not_ne_iff, mem_range]

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