English
Same as above: In a WellFoundedGT α, iSupIndep implies finiteness of index type.
Русский
То же самое: в WellFoundedGT α, iSupIndep имеет вывод о конечности индекса.
LaTeX
$$finite_of_iSupIndep [WellFoundedGT α] {ι : Type*} {t : ι → α} (ht : iSupIndep t) (h_ne_bot : ∀ i, t i ≠ ⊥) : Finite ι$$
Lean4
theorem finite_of_sSupIndep [WellFoundedLT α] {s : Set α} (hs : sSupIndep s) : s.Finite :=
by
by_contra inf
let e := (Infinite.diff inf <| finite_singleton ⊥).to_subtype.natEmbedding
let a n := ⨆ i ≥ n, (e i).1
have sup_le n : (e n).1 ⊔ a (n + 1) ≤ a n :=
sup_le_iff.mpr ⟨le_iSup₂_of_le n le_rfl le_rfl, iSup₂_le fun i hi ↦ le_iSup₂_of_le i (n.le_succ.trans hi) le_rfl⟩
have lt n : a (n + 1) < a n :=
(Disjoint.right_lt_sup_of_left_ne_bot ((hs (e n).2.1).mono_right <| iSup₂_le fun i hi ↦ le_sSup ?_)
(e n).2.2).trans_le
(sup_le n)
· exact (RelEmbedding.natGT a lt).not_wellFounded wellFounded_lt
exact ⟨(e i).2.1, fun h ↦ n.lt_succ_self.not_ge <| hi.trans_eq <| e.2 <| Subtype.val_injective h⟩
