isEmbedding_of_ordConnected — Mathlib

English

An order embedding between linear orders with order topology is a topological embedding if its range is order-connected.

Русский

Вложение порядка между линейными порядками с порядковой топологией является топологическим вложением, если образ диапазона связан по порядку.

LaTeX

$$$f:\\alpha \\hookrightarrow\\beta$ is an IsEmbedding iff range f is OrdConnected.$$

Lean4

/-- An `OrderEmbedding` is a topological embedding provided that the range of `f` is
order-connected -/
theorem isEmbedding_of_ordConnected {α β : Type*} [LinearOrder α] [LinearOrder β] [TopologicalSpace α] [OrderTopology α]
    [TopologicalSpace β] [OrderTopology β] (f : α ↪o β) (hc : OrdConnected (range f)) : Topology.IsEmbedding f :=
  f.strictMono.isEmbedding_of_ordConnected hc

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