range_coe

Mathlib.Topology.Connected.Clopen

URI: https://scilib.ai/kg/mathlib#ConnectedComponents.range_coe

English

The range of mk is the entire ConnectedComponents α; mk is surjective.

Русский

Образ mk равен всей ConnectedComponents(α); mk сюръективно.

LaTeX

$$range\mk = univ$$

Lean4

@[simp]
theorem range_coe : range (mk : α → ConnectedComponents α) = univ :=
  surjective_coe.range_eq

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru