finite_of_iSupIndep — Mathlib

English

In a WellFoundedLT α, if t : ι → α satisfies iSupIndep and no t i is ⊥, then ι is finite.

Русский

В WellFoundedLT α, если t : ι → α удовлетворяет iSupIndep и не существует i, чтобы t i = ⊥, то ι конечна.

LaTeX

$$finite_of_iSupIndep [WellFoundedLT α] {ι : Type*} {t : ι → α} (ht : iSupIndep t) (h_ne_bot : ∀ i, t i ≠ ⊥) : Finite ι$$

Lean4

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

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