English
An injective map pulls back a linear ordered monoid with zero to the domain, yielding a compatible structure on the domain.
Русский
Инъективное отображение тянет линейно упорядоченный моноид с нулем на область определения, создавая совместную структуру на области определения.
LaTeX
$$$\text{If } f:\beta\to\alpha \text{ is injective and preserves 0,1, multiplication, etc., then }\beta \text{ inherits a }\text{LinearOrderedCommMonoidWithZero}$$$
Lean4
/-- Pullback a `LinearOrderedCommMonoidWithZero` under an injective map.
See note [reducible non-instances]. -/
abbrev linearOrderedCommMonoidWithZero {β : Type*} [Zero β] [Bot β] [One β] [Mul β] [Pow β ℕ] [LE β] [LT β] [Max β]
[Min β] [Ord β] [DecidableEq β] [DecidableLE β] [DecidableLT β] (f : β → α) (hf : Function.Injective f)
(zero : f 0 = 0) (one : f 1 = 1) (mul : ∀ x y, f (x * y) = f x * f y) (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n)
(le : ∀ {x y}, f x ≤ f y ↔ x ≤ y) (lt : ∀ {x y}, f x < f y ↔ x < y) (hsup : ∀ x y, f (x ⊔ y) = max (f x) (f y))
(hinf : ∀ x y, f (x ⊓ y) = min (f x) (f y)) (bot : f ⊥ = ⊥) (compare : ∀ x y, compare (f x) (f y) = compare x y) :
LinearOrderedCommMonoidWithZero β
where
__ := hf.linearOrder f le lt hinf hsup compare
__ := hf.commMonoidWithZero f zero one mul npow
__ := Function.Injective.isOrderedMonoid f mul le
zero_le_one := le.1 <| by simp only [zero, one, LinearOrderedCommMonoidWithZero.zero_le_one]
bot_le a := le.1 <| bot ▸ bot_le
