of_subsingleton — Mathlib

English

Let X be a subsingleton. Then any map f : X → Y is inducing; the topology on X coincides with the topology induced by f from Y.

Русский

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

LaTeX

$$$\mathrm{Subsingleton}(X) \Rightarrow \mathrm{IsInducing}(f)$$$

Lean4

theorem of_subsingleton [Subsingleton X] (f : X → Y) : IsInducing f :=
  ⟨Subsingleton.elim _ _⟩

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