English
If s has chainHeight different from top, there exists a well-founded greater-than relation on s.
Русский
Если цепная высота множества s не бесконечна, существует хорошо основанное отношение «больше» на s.
LaTeX
$$s.chainHeight ≠ ⊤ ⇒ WellFoundedGT s$$
Lean4
theorem wellFoundedGT_of_chainHeight_ne_top (s : Set α) (hs : s.chainHeight ≠ ⊤) : WellFoundedGT s :=
by
haveI : IsTrans { x // x ∈ s } (↑· < ↑·) := inferInstance
obtain ⟨n, hn⟩ := WithTop.ne_top_iff_exists.1 hs
refine ⟨RelEmbedding.wellFounded_iff_isEmpty.2 ⟨fun f ↦ ?_⟩⟩
refine n.lt_succ_self.not_ge (WithTop.coe_le_coe.1 <| hn.symm ▸ ?_)
refine
le_iSup₂_of_le ((ofFn (n := n.succ) fun i ↦ f i).map Subtype.val)
⟨isChain_map_of_isChain ((↑) : { x // x ∈ s } → α) (fun _ _ ↦ id)
(isChain_iff_pairwise.2 <| pairwise_ofFn.2 fun i j ↦ f.map_rel_iff.2),
fun i h ↦ ?_⟩
?_
· obtain ⟨a, -, rfl⟩ := mem_map.1 h
exact a.prop
· rw [length_map, length_ofFn]
exact le_rfl
