English
A linear map that sends nonnegative elements to nonnegative elements induces an order homomorphism.
Русский
Линейное отображение, сохраняющее неотрицательность, порождает гомоморфизм по порядку.
LaTeX
$$$\\forall f',\\ \\forall a,b,\\ a \\le b \\Rightarrow f'(a) \\le f'(b)\\ \\,\\text{if } f' \\text{ maps } x \\ge 0 \\text{ to } x \\ge 0$$$
Lean4
/-- A linear map that maps nonnegative elements to nonnegative elements is an order
homomorphism. -/
theorem _root_.OrderHomClass.ofLinear {F' E₁' E₂' : Type*} [FunLike F' E₁' E₂'] [AddCommGroup E₁'] [PartialOrder E₁']
[AddCommGroup E₂'] [PartialOrder E₂'] [Module R E₁'] [Module R E₂'] [LinearMapClass F' R E₁' E₂']
[IsOrderedAddMonoid E₁'] [IsOrderedAddMonoid E₂'] (h : ∀ f : F', ∀ x, 0 ≤ x → 0 ≤ f x) : OrderHomClass F' E₁' E₂'
where
map_rel := by
intro f a b hab
rw [← sub_nonneg] at hab ⊢
have : 0 ≤ f (b - a) := h f (b - a) hab
simpa using this
