isInducing_toContinuousMap — Mathlib

English

The same as above: the map toContinuousMap is inducing; i.e., the domain topology is the initial topology with respect to this map.

Русский

То же самое: отображение toContinuousMap индуцирующее; то есть топология области задаётся исходной топологией относительно этого отображения.

LaTeX

$$⊢ \operatorname{IsInducing}(\mathrm{toContinuousMap} A B).$$

Lean4

@[to_additive]
theorem isInducing_toContinuousMap : IsInducing (toContinuousMap : ContinuousMonoidHom A B → C(A, B)) :=
  ⟨rfl⟩

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