English
iSup f equals lsub f iff every value is strictly below the iSup.
Русский
iSup f равно lsub f тогда и только тогда, когда все значения строго меньше iSup.
LaTeX
$$$iSup f = lsub f \\iff \\forall a < lsub f, \\; succ\\, a < lsub f$$$
Lean4
theorem iSup_eq_lsub_iff {ι} (f : ι → Ordinal) : iSup f = lsub f ↔ ∀ a < lsub f, succ a < lsub f :=
by
refine ⟨fun h => ?_, fun hf => le_antisymm (iSup_le_lsub f) (lsub_le fun i => ?_)⟩
· rw [← h]
exact fun a => succ_lt_iSup_of_ne_iSup fun i => (lsub_le_iff.1 (le_of_eq h.symm) i).ne
by_contra! hle
have heq := (succ_iSup_eq_lsub_iff f).2 ⟨i, le_antisymm (Ordinal.le_iSup _ _) hle⟩
have :=
hf _
(by
rw [← heq]
exact lt_succ (iSup f))
rw [heq] at this
exact this.false
