coinduced_compose — Mathlib

English

Coinducing by g after coinducing by f equals coinducing by g ∘ f: coinduced_g(coinduced_f(t)) = coinduced_{g ∘ f}(t).

Русский

Коиндуцирование через g после коиндуцирования через f совпадает с коиндуцированием через g ∘ f: coinduced_g(coinduced_f(t)) = coinduced_{g ∘ f}(t).

LaTeX

$$$\operatorname{coinduced} g(\operatorname{coinduced} f(t)) = \operatorname{coinduced}_{g \circ f}(t)$$$

Lean4

theorem coinduced_compose [tα : TopologicalSpace α] {f : α → β} {g : β → γ} :
    (tα.coinduced f).coinduced g = tα.coinduced (g ∘ f) :=
  TopologicalSpace.ext rfl

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