wellFoundedLT_of_chainHeight_ne_top

English

If s has chainHeight different from top, then s has a well-founded less-than relation.

Русский

Если цепная высота множества s не бесконечна, то на s существует хорошо основанный порядок «меньше».

LaTeX

$$s.chainHeight ≠ ⊤ ⇒ WellFoundedLT s$$

Lean4

theorem wellFoundedLT_of_chainHeight_ne_top (s : Set α) (hs : s.chainHeight ≠ ⊤) : WellFoundedLT s :=
  wellFoundedGT_of_chainHeight_ne_top (ofDual ⁻¹' s) <| by rwa [chainHeight_dual]

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