induced — Mathlib

English

Let f: X → Y. If X is equipped with the topology induced by f from Y, then f is an inducing map.

Русский

Пусть f: X → Y. Пусть пространство X оснащено топологией, индуцированной через f из Y; тогда f является индуцирующим отображением.

LaTeX

$$$\mathcal{T}_X = \operatorname{induced}_f(\mathcal{T}_Y) \Rightarrow \mathrm{IsInducing}(f).$$$

Lean4

protected theorem induced (f : X → Y) : @IsInducing X Y (induced f ‹_›) _ f :=
  @IsInducing.mk _ _ (TopologicalSpace.induced f ‹_›) _ _ rfl

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