English
Inducing by f after inducing by g equals inducing by g ∘ f: induced_f(induced_g(t)) = induced_{g∘f}(t).
Русский
Индуцирование через f после индуцирования через g эквивалентно индуцированию через g ∘ f: induced_f(induced_g(t)) = induced_{g∘f}(t).
LaTeX
$$$\operatorname{induced} f (\operatorname{induced} g (t)) = \operatorname{induced} (g \circ f) (t)$$$
Lean4
theorem induced_compose {tγ : TopologicalSpace γ} {f : α → β} {g : β → γ} :
(tγ.induced g).induced f = tγ.induced (g ∘ f) :=
TopologicalSpace.ext <|
funext fun _ =>
propext
⟨fun ⟨_, ⟨s, hs, h₂⟩, h₁⟩ => h₁ ▸ h₂ ▸ ⟨s, hs, rfl⟩, fun ⟨s, hs, h⟩ => ⟨preimage g s, ⟨s, hs, rfl⟩, h ▸ rfl⟩⟩
