subsingleton_iff — Mathlib

English

FundamentalGroupoid X is Subsingleton iff X is Subsingleton.

Русский

FundamentalGroupoid X является Subsingleton тогда и только тогда, когда X является Subsingleton.

LaTeX

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

Lean4

@[simp]
theorem subsingleton_iff (X : Type*) : Subsingleton (FundamentalGroupoid X) ↔ Subsingleton X :=
  equiv _ |>.subsingleton_congr

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