English
For a family 𝔖 of subsets of ι, the induced topology on 𝔖.sUnion.restrict Pi.topologicalSpace equals the infimum over S ∈ 𝔖 of induced topologies on S.restrict.
Русский
Для семейства 𝔖 подмножеств ι индуцированная топология на 𝔖.sUnion.restrict Pi.topologicalSpace равна инфимума по S ∈ 𝔖 индуцированным топологиям на S.restrict.
LaTeX
$$$\operatorname{Induced}(\,\bigcup_{S\in\mathcal{S}} S\text{.restrict},\Pi\text{topologicalSpace}) = \bigwedge_{S\in\mathcal{S}} \operatorname{Induced}(S\text{.restrict},\Pi\text{topologicalSpace}).$$$
Lean4
@[continuity, fun_prop]
theorem continuous_restrict₂_apply {s t : Set X} (hst : s ⊆ t) {f : t → Z} (hf : Continuous f) :
Continuous (restrict₂ (π := fun _ ↦ Z) hst f) :=
hf.comp (continuous_inclusion hst)
