English
If t is an independent indexed family and f is an injective function between index sets, then t ∘ f is independent.
Русский
Если t — независимая индексированная семья и f — инъекция между индексными множествами, тогда t ∘ f является независимой.
LaTeX
$$$\\\\forall t,f,\\\\ iSupIndep(t) \\\\land (Injective(f)) \\\\Rightarrow iSupIndep(t \\circ f)$$$
Lean4
/-- Composing an independent indexed family with an injective function on the index results in
another independent indexed family. -/
theorem comp {ι ι' : Sort*} {t : ι → α} {f : ι' → ι} (ht : iSupIndep t) (hf : Injective f) : iSupIndep (t ∘ f) :=
fun i =>
(ht (f i)).mono_right <| by
refine (iSup_mono fun i => ?_).trans (iSup_comp_le _ f)
exact iSup_const_mono hf.ne
