of_sequentialSpace — Mathlib

English

Every sequential space is compactly coherent.

Русский

Каждое последовательное пространство компактно-согласовано.

LaTeX

$$$ \text{SequentialSpace}(X) \Rightarrow \operatorname{CompactlyCoherentSpace}(X) $$$

Lean4

/-- Every sequential space is a compactly coherent space. -/
instance of_sequentialSpace [SequentialSpace X] : CompactlyCoherentSpace X where
  isCoherentWith := IsCoherentWith.of_seq fun _u _x hux ↦ hux.isCompact_insert_range

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