English
For any fixed element b in the submonoid, there is an order-embedding of α into Localization(s) sending a to the fraction a/b, thus realizing α as a subordered set of the localization.
Русский
Для фиксированного элемента b из подмоноида существует вложение порядка из α в Localization(s), отправляющее a в дробь a/b, тем самым отображая α в подпорядкованное множество локализации.
LaTeX
$$\\(\\iota_b: \\alpha \\hookrightarrow_o \\operatorname{Localization}(s), \\quad \\iota_b(a) = a/b\\)$$
Lean4
/-- An ordered cancellative monoid injects into its localization by sending `a` to `a / b`. -/
@[to_additive (attr := simps!) /-- An ordered cancellative monoid injects into its localization by
sending `a` to `a - b`. -/
]
def mkOrderEmbedding (b : s) : α ↪o Localization s
where
toFun a := mk a b
inj' := mk_left_injective _
map_rel_iff' {a b} := by simp [mk_le_mk]
