instArchimedean — Mathlib

English

The subtype of nonnegative elements inherits Archimedean property.

Русский

Подмножество неотрицательных элементов наследует архимедово свойство.

LaTeX

$$$$ \operatorname{Archimedean}\bigl(\{ x \in M \mid x \ge 0 \}\bigr). $$$$

Lean4

instance instArchimedean (M) [AddCommMonoid M] [PartialOrder M] [Archimedean M] : Archimedean (WithBot M) :=
  by
  constructor
  intro x y hxy
  cases y with
  | bot => exact absurd hxy bot_le.not_gt
  | coe y =>
    cases x with
    | bot => refine ⟨0, bot_le⟩
    | coe x => simpa [← WithBot.coe_nsmul] using (Archimedean.arch x (by simpa using hxy))

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