Theorems · Theorem · order theory

Set.pairwise_disjoint_Ioc_add_zsmul

∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α] (a b : α),
  Pairwise (Function.onFun Disjoint fun n => Set.Ioc (a + n • b) (a + (n + 1) • b))

Defined in

Mathlib.Algebra.Order.Interval.Set.Group

Cited by

3 results in Mathlib

Foundations

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

Assumes

AddCommGroupPartialOrderIsOrderedAddMonoid