strictMono_topEquiv — Mathlib

English

The canonical order-preserving map from the top element of the topological-like substructure to the base structure is strictly increasing.

Русский

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

LaTeX

$$StrictMono( topEquiv (M := G) )$$

Lean4

@[to_additive]
theorem strictMono_topEquiv {G : Type*} [CommMonoid G] [PartialOrder G] : StrictMono (topEquiv (M := G)) := fun _ _ ↦ id

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