English
If a ≥ 0 in α, then algebraMap α β a ≥ 0 in β; a consequence of monotonicity.
Русский
Если a ≥ 0 в α, то algebraMap α β a ≥ 0 в β; следствие монотонности.
LaTeX
$$$a \ge 0 \Rightarrow \text{algebraMap } a \ge 0$$$
Lean4
/-- Given an upper set `s` of archimedean classes in a linearly ordered module `M` with Archimedean
scalars, all elements belonging to these classes form a submodule, except when `s = ⊤` for which the
set would be empty. For `s = ⊤`, we assign the junk value `⊥`.
This has the same carrier as `ArchimedeanClass.addSubgroup`'s. -/
noncomputable def submodule (s : UpperSet (ArchimedeanClass M)) : Submodule K M
where
__ := addSubgroup s
smul_mem' k
{a} := by
obtain rfl | hs := eq_or_ne s ⊤
· aesop
simpa [mem_addSubgroup_iff hs] using s.upper (mk_le_mk_smul a k)
