nonempty_iff

Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic

URI: https://scilib.ai/kg/mathlib#FundamentalGroupoid.nonempty_iff

English

Nonempty (FundamentalGroupoid X) iff Nonempty X.

Русский

Непустота фундаментального группоида эквивалентна не пустоте X.

LaTeX

$$$$ \\operatorname{Nonempty}(\\mathrm{FundamentalGroupoid}(X)) \\iff \\operatorname{Nonempty}(X). $$$$

Lean4

@[simp]
theorem nonempty_iff (X : Type*) : Nonempty (FundamentalGroupoid X) ↔ Nonempty X :=
  equiv _ |>.nonempty_congr

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

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

Разделы

Аффилиация

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