of_coe_Iic_comp — Mathlib

English

If the iSupIndep of the coerced family t into α holds, then iSupIndep holds for t valued in Set.Iic a.

Русский

Если iSupIndep от семейства t с приведением в α, то iSupIndep для t, рассматриваемого как элементы Set.Iic a, верно.

LaTeX

$$$iSupIndep ((↑) \\circ t) \\\\Rightarrow iSupIndep t$$$

Lean4

theorem of_coe_Iic_comp {ι : Sort*} {a : α} {t : ι → Set.Iic a} (ht : iSupIndep ((↑) ∘ t : ι → α)) : iSupIndep t :=
  by
  intro i x
  specialize ht i
  simp_rw [Function.comp_apply, ← Set.Iic.coe_iSup] at ht
  exact @ht x

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