sSupIndep_range — Mathlib

English

If t is an independent indexed family, then its range is independent.

Русский

Если t — независимая индексированная семья, то её образ (множество значений) является независимым.

LaTeX

$$$\\\\forall t: ι \\to α,\\\\ iSupIndep(t) \\\\Rightarrow sSupIndep(\\\\text{range } t)$$$

Lean4

theorem sSupIndep_range (ht : iSupIndep t) : sSupIndep <| range t :=
  by
  rw [sSupIndep_iff]
  rw [← coe_comp_rangeFactorization t] at ht
  exact ht.comp' rangeFactorization_surjective

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