mk — Mathlib · SciLib

English

The natural projection map sends each point to its connected component class: mk(x) is the class of x.

Русский

Естественное отображение mk отправляет каждую точку в её класс связной компоненты: mk(x) = [x].

LaTeX

$$\operatorname{mk}(x) = [x]$$

Lean4

/-- Coercion from a topological space to the set of connected components of this space. -/
def mk : α → ConnectedComponents α :=
  Quotient.mk''

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