finite_of_iSupIndep — Mathlib

English

In a WellFoundedLT α, sSupIndep s implies s is finite.

Русский

В WellFoundedLT α, sSupIndep s означает конечность s.

LaTeX

$$finite_of_sSupIndep [WellFoundedLT α] {s : Set α} (hs : sSupIndep s) : s.Finite$$

Lean4

theorem finite_of_iSupIndep [WellFoundedLT α] {ι : Type*} {t : ι → α} (ht : iSupIndep t) (h_ne_bot : ∀ i, t i ≠ ⊥) :
    Finite ι :=
  haveI := (WellFoundedLT.finite_of_sSupIndep ht.sSupIndep_range).to_subtype
  Finite.of_injective_finite_range (ht.injective h_ne_bot)

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