discreteIsConnectedEquivPUnit — Mathlib

English

If the discrete category on α is connected, then α is equivalent to the one-point type PUnit.

Русский

Если дискретная категория на α связна, то α эквивалентна типу с одним элементом PUnit.

LaTeX

$$$[IsConnected(Discrete(\\alpha))] \\Rightarrow (\\alpha \\simeq PUnit)$$

Lean4

/-- If `Discrete α` is connected, then `α` is (type-)equivalent to `PUnit`. -/
def discreteIsConnectedEquivPUnit {α : Type u₁} [IsConnected (Discrete α)] : α ≃ PUnit :=
  Discrete.equivOfEquivalence.{u₁, u₁}
    { functor := Functor.star (Discrete α)
      inverse := Discrete.functor fun _ => Classical.arbitrary _
      unitIso := isoConstant _ (Classical.arbitrary _)
      counitIso := Functor.punitExt _ _ }

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