coinduced_iSup — Mathlib

English

Coinduced distributes over directed supremum: coinduced f (iSup t) = iSup (coinduced f t).

Русский

Коиндуцированная по f распределяется по iSup: coinduced f (iSup t) = iSup (coinduced f t).

LaTeX

$$$\operatorname{coinduced} f \left(\iSup i, t_i\right) = \iSup i, \operatorname{coinduced} f(t_i)$$$

Lean4

@[simp]
theorem coinduced_iSup {ι : Sort w} {t : ι → TopologicalSpace α} : (⨆ i, t i).coinduced f = ⨆ i, (t i).coinduced f :=
  (gc_coinduced_induced f).l_iSup

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