Mathlib.Algebra.Order.Monoid.Unbundled.ExistsOfLE

ExistsAddOfLE structure

(α : Type u) [Add α] [LE α]

Full source

/-- An `OrderedAddCommMonoid` with one-sided 'subtraction' in the sense that
if `a ≤ b`, then there is some `c` for which `a + c = b`. This is a weaker version
of the condition on canonical orderings defined by `CanonicallyOrderedAddCommMonoid`. -/
class ExistsAddOfLE (α : Type u) [Add α] [LE α] : Prop where
  /-- For `a ≤ b`, there is a `c` so `b = a + c`. -/
  exists_add_of_le : ∀ {a b : α}, a ≤ b → ∃ c : α, b = a + c

Ordered additive commutative monoid with one-sided subtraction

Informal description

An ordered additive commutative monoid with a one-sided 'subtraction' property: for any elements $ a $ and $ b $ with $ a \leq b $, there exists an element $ c $ such that $ a + c = b $. This is a weaker version of the condition defining canonically ordered additive commutative monoids.

ExistsMulOfLE structure

(α : Type u) [Mul α] [LE α]

Full source

/-- An `OrderedCommMonoid` with one-sided 'division' in the sense that
if `a ≤ b`, there is some `c` for which `a * c = b`. This is a weaker version
of the condition on canonical orderings defined by `CanonicallyOrderedCommMonoid`. -/
@[to_additive]
class ExistsMulOfLE (α : Type u) [Mul α] [LE α] : Prop where
  /-- For `a ≤ b`, `a` left divides `b` -/
  exists_mul_of_le : ∀ {a b : α}, a ≤ b → ∃ c : α, b = a * c

Ordered commutative monoid with one-sided division

Informal description

An ordered commutative monoid with a one-sided 'division' property: for any elements $ a $ and $ b $ with $ a \leq b $, there exists an element $ c $ such that $ a \cdot c = b $. This is a weaker version of the condition defining canonically ordered commutative monoids.

Group.existsMulOfLE instance

(α : Type u) [Group α] [LE α] : ExistsMulOfLE α

Full source

@[to_additive]
instance (priority := 100) Group.existsMulOfLE (α : Type u) [Group α] [LE α] : ExistsMulOfLE α :=
  ⟨fun {a b} _ => ⟨a⁻¹ * b, (mul_inv_cancel_left _ _).symm⟩⟩

Groups Satisfy the One-Sided Division Property for Preorders

Informal description

Every group $\alpha$ with a preorder $\leq$ satisfies the property that for any elements $a, b \in \alpha$ with $a \leq b$, there exists an element $c \in \alpha$ such that $a \cdot c = b$.

exists_one_le_mul_of_le theorem

[MulLeftReflectLE α] (h : a ≤ b) : ∃ c, 1 ≤ c ∧ a * c = b

Full source

@[to_additive] lemma exists_one_le_mul_of_le [MulLeftReflectLE α] (h : a ≤ b) :
    ∃ c, 1 ≤ c ∧ a * c = b := by
  obtain ⟨c, rfl⟩ := exists_mul_of_le h; exact ⟨c, one_le_of_le_mul_right h, rfl⟩

Existence of positive multiplicative factor for order relation in monoids

Informal description

Let $\alpha$ be a monoid with a preorder $\leq$ such that multiplication on the left reflects the order (i.e., $a \leq b$ implies there exists $c$ with $a \cdot c = b$). Then for any elements $a, b \in \alpha$ with $a \leq b$, there exists an element $c \in \alpha$ such that $1 \leq c$ and $a \cdot c = b$.

exists_one_lt_mul_of_lt' theorem

[MulLeftReflectLT α] (h : a < b) : ∃ c, 1 < c ∧ a * c = b

Full source

@[to_additive] lemma exists_one_lt_mul_of_lt' [MulLeftReflectLT α] (h : a < b) :
    ∃ c, 1 < c ∧ a * c = b := by
  obtain ⟨c, rfl⟩ := exists_mul_of_le h.le; exact ⟨c, one_lt_of_lt_mul_right h, rfl⟩

Existence of strictly positive multiplicative factor for strict order relation in monoids

Informal description

Let $\alpha$ be a monoid with a preorder $\leq$ such that multiplication on the left reflects the strict order (i.e., $a < b$ implies there exists $c$ with $a \cdot c = b$). Then for any elements $a, b \in \alpha$ with $a < b$, there exists an element $c \in \alpha$ such that $1 < c$ and $a \cdot c = b$.

le_iff_exists_one_le_mul theorem

[MulLeftMono α] [MulLeftReflectLE α] : a ≤ b ↔ ∃ c, 1 ≤ c ∧ a * c = b

Full source

@[to_additive] lemma le_iff_exists_one_le_mul [MulLeftMono α]
    [MulLeftReflectLE α] : a ≤ b ↔ ∃ c, 1 ≤ c ∧ a * c = b :=
  ⟨exists_one_le_mul_of_le, by rintro ⟨c, hc, rfl⟩; exact le_mul_of_one_le_right' hc⟩

Order Relation Characterized by Multiplicative Factor in Monoids

Informal description

Let $\alpha$ be a monoid with a preorder $\leq$ such that multiplication on the left is monotone and reflects the order. Then for any elements $a, b \in \alpha$, we have $a \leq b$ if and only if there exists an element $c \in \alpha$ such that $1 \leq c$ and $a \cdot c = b$.

lt_iff_exists_one_lt_mul theorem

[MulLeftStrictMono α] [MulLeftReflectLT α] : a < b ↔ ∃ c, 1 < c ∧ a * c = b

Full source

@[to_additive] lemma lt_iff_exists_one_lt_mul [MulLeftStrictMono α]
    [MulLeftReflectLT α] : a < b ↔ ∃ c, 1 < c ∧ a * c = b :=
  ⟨exists_one_lt_mul_of_lt', by rintro ⟨c, hc, rfl⟩; exact lt_mul_of_one_lt_right' _ hc⟩

Characterization of Strict Order via Multiplicative Factor in Monoids

Informal description

Let $\alpha$ be a monoid with a preorder $\leq$ such that multiplication on the left is strictly monotone and reflects the strict order. Then for any elements $a, b \in \alpha$, we have $a < b$ if and only if there exists an element $c \in \alpha$ such that $1 < c$ and $a \cdot c = b$.

le_of_forall_one_lt_le_mul theorem

(h : ∀ ε : α, 1 < ε → a ≤ b * ε) : a ≤ b

Full source

@[to_additive]
theorem le_of_forall_one_lt_le_mul (h : ∀ ε : α, 1 < ε → a ≤ b * ε) : a ≤ b :=
  le_of_forall_gt_imp_ge_of_dense fun x hxb => by
    obtain ⟨ε, rfl⟩ := exists_mul_of_le hxb.le
    exact h _ (one_lt_of_lt_mul_right hxb)

Order Criterion via Multiplicative Factors in Monoids: $\forall \epsilon>1, a \leq b \cdot \epsilon \Rightarrow a \leq b$

Informal description

Let $\alpha$ be a monoid with a preorder $\leq$ such that multiplication on the left is monotone. For any elements $a, b \in \alpha$, if for every $\epsilon \in \alpha$ with $1 < \epsilon$ we have $a \leq b \cdot \epsilon$, then $a \leq b$.

le_of_forall_one_lt_lt_mul' theorem

(h : ∀ ε : α, 1 < ε → a < b * ε) : a ≤ b

Full source

@[to_additive]
theorem le_of_forall_one_lt_lt_mul' (h : ∀ ε : α, 1 < ε → a < b * ε) : a ≤ b :=
  le_of_forall_one_lt_le_mul fun ε hε => (h ε hε).le

Order Criterion via Strict Multiplicative Factors in Monoids: $\forall \epsilon>1, a < b \cdot \epsilon \Rightarrow a \leq b$

Informal description

Let $\alpha$ be a monoid with a preorder $\leq$ such that multiplication on the left is strictly monotone. For any elements $a, b \in \alpha$, if for every $\epsilon \in \alpha$ with $1 < \epsilon$ we have $a < b \cdot \epsilon$, then $a \leq b$.

le_iff_forall_one_lt_lt_mul' theorem

[MulLeftStrictMono α] : a ≤ b ↔ ∀ ε, 1 < ε → a < b * ε

Full source

@[to_additive]
theorem le_iff_forall_one_lt_lt_mul' [MulLeftStrictMono α] :
    a ≤ b ↔ ∀ ε, 1 < ε → a < b * ε :=
  ⟨fun h _ => lt_mul_of_le_of_one_lt h, le_of_forall_one_lt_lt_mul'⟩

Order Characterization via Strict Multiplicative Factors in Monoids: $a \leq b \leftrightarrow \forall \epsilon>1, a < b \cdot \epsilon$

Informal description

Let $\alpha$ be a monoid with a preorder $\leq$ such that multiplication on the left is strictly monotone. For any elements $a, b \in \alpha$, the inequality $a \leq b$ holds if and only if for every $\epsilon \in \alpha$ with $1 < \epsilon$, we have $a < b \cdot \epsilon$.

le_iff_forall_one_lt_le_mul theorem

[MulLeftStrictMono α] : a ≤ b ↔ ∀ ε, 1 < ε → a ≤ b * ε

Full source

@[to_additive]
theorem le_iff_forall_one_lt_le_mul [MulLeftStrictMono α] :
    a ≤ b ↔ ∀ ε, 1 < ε → a ≤ b * ε :=
  ⟨fun h _ hε ↦ lt_mul_of_le_of_one_lt h hε |>.le, le_of_forall_one_lt_le_mul⟩

Order Characterization via Multiplicative Factors in Monoids: $a \leq b \leftrightarrow \forall \epsilon>1, a \leq b \cdot \epsilon$

Informal description

Let $\alpha$ be a monoid with a preorder $\leq$ such that multiplication on the left is strictly monotone. For any elements $a, b \in \alpha$, the inequality $a \leq b$ holds if and only if for every $\epsilon \in \alpha$ with $1 < \epsilon$, we have $a \leq b \cdot \epsilon$.