totallyDisconnectedSpace_subtype_iff

English

For any subset s, TotallyDisconnectedSpace s is equivalent to IsTotallyDisconnected s.

Русский

Для любого подмножества s пространство подтипа s полностью раздельно тогда и только тогда, когда s полностью раздельно.

LaTeX

$$TotallyDisconnectedSpace s ↔ IsTotallyDisconnected s$$

Lean4

theorem totallyDisconnectedSpace_subtype_iff {s : Set α} : TotallyDisconnectedSpace s ↔ IsTotallyDisconnected s := by
  rw [← IsEmbedding.subtypeVal.isTotallyDisconnected_range, Subtype.range_val]

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