finite_ne_bot_of_iSupIndep — Mathlib

English

In a WellFoundedGT α, if t : ι → α is iSupIndep with all t i ≠ ⊥, then ι is finite.

Русский

В WellFoundedGT α, если t : ι → α удовлетворяет iSupIndep и каждый t i ≠ ⊥, то ι конечно.

LaTeX

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

Lean4

theorem finite_ne_bot_of_iSupIndep [WellFoundedGT α] {ι : Type*} {t : ι → α} (ht : iSupIndep t) :
    Set.Finite {i | t i ≠ ⊥} :=
  by
  refine Finite.of_finite_image (Finite.subset ?_ (image_subset_range t _)) ht.injOn
  exact WellFoundedGT.finite_of_sSupIndep ht.sSupIndep_range

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