Theorems · Theorem · general topology

Set.Icc.addNSMul_eq_right

∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [IsOrderedAddMonoid α] {a b : α} (h : a ≤ b) {δ : α}
  [Archimedean α], 0 < δ → ∃ m, ∀ n ≥ m, ↑(Set.Icc.addNSMul h δ n) = b

Defined in

Mathlib.Topology.UnitInterval

Cited by

2 results in Mathlib

Foundations

Depth 27 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

AddCommGroupLinearOrderIsOrderedAddMonoidArchimedean