infiniteDimensionalOrder_of_strictMono

English

If f: α → β is strictly monotone and α is infinite-dimensional, then β is infinite-dimensional.

Русский

Если f: α → β строго монотонна и α бесконечно размерна, то β также бесконечно размерен.

LaTeX

$$$\\forall f:\\,\\alpha \\to \\beta,\\; (\\text{StrictMono}(f)) \\land [InfiniteDimensionalOrder(\\alpha)] \\rightarrow InfiniteDimensionalOrder(\\beta)$$$

Lean4

/-- If `f : α → β` is a strictly monotonic function and `α` is an infinite-dimensional type then so
  is `β`. -/
theorem infiniteDimensionalOrder_of_strictMono [Preorder α] [Preorder β] (f : α → β) (hf : StrictMono f)
    [InfiniteDimensionalOrder α] : InfiniteDimensionalOrder β :=
  ⟨fun n ↦ ⟨(LTSeries.withLength _ n).map f hf, LTSeries.length_withLength α n⟩⟩

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