succ_iSup_le_lsub_iff — Mathlib

English

succ(iSup f) ≤ lsub f iff there exists i with f i = iSup f.

Русский

succ(iSup f) ≤ lsub f эквивалентно существованию i such that f i = iSup f.

LaTeX

$$$\\operatorname{succ}(iSup f) \\le lsub f \\iff \\exists i, f(i) = iSup f$$$

Lean4

theorem succ_iSup_le_lsub_iff {ι} (f : ι → Ordinal) : succ (iSup f) ≤ lsub f ↔ ∃ i, f i = iSup f :=
  by
  refine ⟨fun h => ?_, ?_⟩
  · by_contra! hf
    have := forall_congr' fun i ↦ (Ordinal.le_iSup f i).lt_iff_ne.symm
    exact (succ_le_iff.1 h).ne ((iSup_le_lsub f).antisymm (lsub_le (this.1 hf)))
  rintro ⟨_, hf⟩
  rw [succ_le_iff, ← hf]
  exact lt_lsub _ _

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