Mathlib.Algebra.Order.Interval.Set.Group

Set.inv_mem_Icc_iff theorem

: a⁻¹ ∈ Set.Icc c d ↔ a ∈ Set.Icc d⁻¹ c⁻¹

Full source

@[to_additive]
theorem inv_mem_Icc_iff : a⁻¹a⁻¹ ∈ Set.Icc c da⁻¹ ∈ Set.Icc c d ↔ a ∈ Set.Icc d⁻¹ c⁻¹ :=
  and_comm.trans <| and_congr inv_le' le_inv'

Inverse Membership in Closed Interval: $a^{-1} \in [c, d] \leftrightarrow a \in [d^{-1}, c^{-1}]$

Informal description

For any elements $a, c, d$ in an ordered group, the inverse $a^{-1}$ belongs to the closed interval $[c, d]$ if and only if $a$ belongs to the closed interval $[d^{-1}, c^{-1}]$.

Set.inv_mem_Ico_iff theorem

: a⁻¹ ∈ Set.Ico c d ↔ a ∈ Set.Ioc d⁻¹ c⁻¹

Full source

@[to_additive]
theorem inv_mem_Ico_iff : a⁻¹a⁻¹ ∈ Set.Ico c da⁻¹ ∈ Set.Ico c d ↔ a ∈ Set.Ioc d⁻¹ c⁻¹ :=
  and_comm.trans <| and_congr inv_lt' le_inv'

Inverse Membership in Left-Closed Right-Open Interval: $a^{-1} \in [c, d) \leftrightarrow a \in (d^{-1}, c^{-1}]$

Informal description

For any elements $a, c, d$ in an ordered group, the inverse $a^{-1}$ belongs to the left-closed right-open interval $[c, d)$ if and only if $a$ belongs to the left-open right-closed interval $(d^{-1}, c^{-1}]$.

Set.inv_mem_Ioc_iff theorem

: a⁻¹ ∈ Set.Ioc c d ↔ a ∈ Set.Ico d⁻¹ c⁻¹

Full source

@[to_additive]
theorem inv_mem_Ioc_iff : a⁻¹a⁻¹ ∈ Set.Ioc c da⁻¹ ∈ Set.Ioc c d ↔ a ∈ Set.Ico d⁻¹ c⁻¹ :=
  and_comm.trans <| and_congr inv_le' lt_inv'

Inverse Membership in Left-Open Right-Closed Interval: $a^{-1} \in (c, d] \leftrightarrow a \in [d^{-1}, c^{-1})$

Informal description

For any elements $a, c, d$ in an ordered group, the inverse $a^{-1}$ belongs to the left-open right-closed interval $(c, d]$ if and only if $a$ belongs to the left-closed right-open interval $[d^{-1}, c^{-1})$.

Set.inv_mem_Ioo_iff theorem

: a⁻¹ ∈ Set.Ioo c d ↔ a ∈ Set.Ioo d⁻¹ c⁻¹

Full source

@[to_additive]
theorem inv_mem_Ioo_iff : a⁻¹a⁻¹ ∈ Set.Ioo c da⁻¹ ∈ Set.Ioo c d ↔ a ∈ Set.Ioo d⁻¹ c⁻¹ :=
  and_comm.trans <| and_congr inv_lt' lt_inv'

Inverse Membership in Open Interval: $a^{-1} \in (c, d) \leftrightarrow a \in (d^{-1}, c^{-1})$

Informal description

For any elements $a, c, d$ in an ordered group, the inverse $a^{-1}$ belongs to the open interval $(c, d)$ if and only if $a$ belongs to the open interval $(d^{-1}, c^{-1})$.

Set.add_mem_Icc_iff_left theorem

: a + b ∈ Set.Icc c d ↔ a ∈ Set.Icc (c - b) (d - b)

Full source

theorem add_mem_Icc_iff_left : a + b ∈ Set.Icc c da + b ∈ Set.Icc c d ↔ a ∈ Set.Icc (c - b) (d - b) :=
  (and_congr sub_le_iff_le_add le_sub_iff_add_le).symm

Translation of Sum in Closed Interval via Left Argument

Informal description

For elements $a, b, c, d$ in an ordered additive monoid $\alpha$, the sum $a + b$ lies in the closed interval $[c, d]$ if and only if $a$ lies in the closed interval $[c - b, d - b]$.

Set.add_mem_Ico_iff_left theorem

: a + b ∈ Set.Ico c d ↔ a ∈ Set.Ico (c - b) (d - b)

Full source

theorem add_mem_Ico_iff_left : a + b ∈ Set.Ico c da + b ∈ Set.Ico c d ↔ a ∈ Set.Ico (c - b) (d - b) :=
  (and_congr sub_le_iff_le_add lt_sub_iff_add_lt).symm

Translation Invariance of Left-Closed Right-Open Interval Membership for Left Summand

Informal description

For elements $a, b, c, d$ in an ordered additive monoid $\alpha$, the sum $a + b$ lies in the left-closed right-open interval $[c, d)$ if and only if $a$ lies in the left-closed right-open interval $[c - b, d - b)$. That is, \[ a + b \in [c, d) \iff a \in [c - b, d - b). \]

Set.add_mem_Ioc_iff_left theorem

: a + b ∈ Set.Ioc c d ↔ a ∈ Set.Ioc (c - b) (d - b)

Full source

theorem add_mem_Ioc_iff_left : a + b ∈ Set.Ioc c da + b ∈ Set.Ioc c d ↔ a ∈ Set.Ioc (c - b) (d - b) :=
  (and_congr sub_lt_iff_lt_add le_sub_iff_add_le).symm

Translation Invariance of Left-Open Right-Closed Interval Membership for Left Summand

Informal description

For elements $a, b, c, d$ in an ordered additive monoid $\alpha$, the sum $a + b$ lies in the left-open right-closed interval $(c, d]$ if and only if $a$ lies in the left-open right-closed interval $(c - b, d - b]$. That is, \[ a + b \in (c, d] \iff a \in (c - b, d - b]. \]

Set.add_mem_Ioo_iff_left theorem

: a + b ∈ Set.Ioo c d ↔ a ∈ Set.Ioo (c - b) (d - b)

Full source

theorem add_mem_Ioo_iff_left : a + b ∈ Set.Ioo c da + b ∈ Set.Ioo c d ↔ a ∈ Set.Ioo (c - b) (d - b) :=
  (and_congr sub_lt_iff_lt_add lt_sub_iff_add_lt).symm

Translation Invariance of Open Interval Membership for Left Summand

Informal description

For elements $a, b, c, d$ in an ordered additive monoid $\alpha$, the sum $a + b$ lies in the open interval $(c, d)$ if and only if $a$ lies in the open interval $(c - b, d - b)$. That is, \[ a + b \in (c, d) \iff a \in (c - b, d - b). \]

Set.add_mem_Icc_iff_right theorem

: a + b ∈ Set.Icc c d ↔ b ∈ Set.Icc (c - a) (d - a)

Full source

theorem add_mem_Icc_iff_right : a + b ∈ Set.Icc c da + b ∈ Set.Icc c d ↔ b ∈ Set.Icc (c - a) (d - a) :=
  (and_congr sub_le_iff_le_add' le_sub_iff_add_le').symm

Translation Invariance of Closed Interval Membership for Right Summand

Informal description

For elements $a, b, c, d$ in an ordered additive monoid $\alpha$, the sum $a + b$ lies in the closed interval $[c, d]$ if and only if $b$ lies in the closed interval $[c - a, d - a]$. That is, \[ a + b \in [c, d] \iff b \in [c - a, d - a]. \]

Set.add_mem_Ico_iff_right theorem

: a + b ∈ Set.Ico c d ↔ b ∈ Set.Ico (c - a) (d - a)

Full source

theorem add_mem_Ico_iff_right : a + b ∈ Set.Ico c da + b ∈ Set.Ico c d ↔ b ∈ Set.Ico (c - a) (d - a) :=
  (and_congr sub_le_iff_le_add' lt_sub_iff_add_lt').symm

Translation Invariance of Left-Closed Right-Open Interval Membership for Right Summand

Informal description

For elements $a, b, c, d$ in an ordered additive monoid $\alpha$, the sum $a + b$ lies in the left-closed right-open interval $[c, d)$ if and only if $b$ lies in the left-closed right-open interval $[c - a, d - a)$. That is, \[ a + b \in [c, d) \iff b \in [c - a, d - a). \]

Set.add_mem_Ioc_iff_right theorem

: a + b ∈ Set.Ioc c d ↔ b ∈ Set.Ioc (c - a) (d - a)

Full source

theorem add_mem_Ioc_iff_right : a + b ∈ Set.Ioc c da + b ∈ Set.Ioc c d ↔ b ∈ Set.Ioc (c - a) (d - a) :=
  (and_congr sub_lt_iff_lt_add' le_sub_iff_add_le').symm

Translation Invariance of Left-Open Right-Closed Interval Membership for Right Summand

Informal description

For elements $a, b, c, d$ in an ordered additive monoid $\alpha$, the sum $a + b$ lies in the left-open right-closed interval $(c, d]$ if and only if $b$ lies in the left-open right-closed interval $(c - a, d - a]$. That is, \[ a + b \in (c, d] \iff b \in (c - a, d - a]. \]

Set.add_mem_Ioo_iff_right theorem

: a + b ∈ Set.Ioo c d ↔ b ∈ Set.Ioo (c - a) (d - a)

Full source

theorem add_mem_Ioo_iff_right : a + b ∈ Set.Ioo c da + b ∈ Set.Ioo c d ↔ b ∈ Set.Ioo (c - a) (d - a) :=
  (and_congr sub_lt_iff_lt_add' lt_sub_iff_add_lt').symm

Translation of Open Interval Membership under Addition: Right Version

Informal description

For elements $a, b, c, d$ in an ordered additive monoid $\alpha$, the sum $a + b$ lies in the open interval $(c, d)$ if and only if $b$ lies in the open interval $(c - a, d - a)$. That is, \[ a + b \in (c, d) \iff b \in (c - a, d - a). \]

Set.sub_mem_Icc_iff_left theorem

: a - b ∈ Set.Icc c d ↔ a ∈ Set.Icc (c + b) (d + b)

Full source

theorem sub_mem_Icc_iff_left : a - b ∈ Set.Icc c da - b ∈ Set.Icc c d ↔ a ∈ Set.Icc (c + b) (d + b) :=
  and_congr le_sub_iff_add_le sub_le_iff_le_add

Translation of Interval Membership under Subtraction: Left Version

Informal description

For elements $a, b, c, d$ in an ordered additive monoid $\alpha$, the difference $a - b$ lies in the closed interval $[c, d]$ if and only if $a$ lies in the closed interval $[c + b, d + b]$. That is, \[ a - b \in [c, d] \iff a \in [c + b, d + b]. \]

Set.sub_mem_Ico_iff_left theorem

: a - b ∈ Set.Ico c d ↔ a ∈ Set.Ico (c + b) (d + b)

Full source

theorem sub_mem_Ico_iff_left : a - b ∈ Set.Ico c da - b ∈ Set.Ico c d ↔ a ∈ Set.Ico (c + b) (d + b) :=
  and_congr le_sub_iff_add_le sub_lt_iff_lt_add

Translation of Left-Closed Right-Open Interval Membership under Subtraction: Left Version

Informal description

For elements $a, b, c, d$ in an ordered additive monoid $\alpha$, the difference $a - b$ lies in the left-closed right-open interval $[c, d)$ if and only if $a$ lies in the left-closed right-open interval $[c + b, d + b)$. That is, \[ a - b \in [c, d) \iff a \in [c + b, d + b). \]

Set.sub_mem_Ioc_iff_left theorem

: a - b ∈ Set.Ioc c d ↔ a ∈ Set.Ioc (c + b) (d + b)

Full source

theorem sub_mem_Ioc_iff_left : a - b ∈ Set.Ioc c da - b ∈ Set.Ioc c d ↔ a ∈ Set.Ioc (c + b) (d + b) :=
  and_congr lt_sub_iff_add_lt sub_le_iff_le_add

Translation of Left-Open Right-Closed Interval Membership under Subtraction: Left Version

Informal description

For elements $a, b, c, d$ in an ordered additive monoid $\alpha$, the difference $a - b$ lies in the left-open right-closed interval $(c, d]$ if and only if $a$ lies in the left-open right-closed interval $(c + b, d + b]$. That is, \[ a - b \in (c, d] \iff a \in (c + b, d + b]. \]

Set.sub_mem_Ioo_iff_left theorem

: a - b ∈ Set.Ioo c d ↔ a ∈ Set.Ioo (c + b) (d + b)

Full source

theorem sub_mem_Ioo_iff_left : a - b ∈ Set.Ioo c da - b ∈ Set.Ioo c d ↔ a ∈ Set.Ioo (c + b) (d + b) :=
  and_congr lt_sub_iff_add_lt sub_lt_iff_lt_add

Translation of Open Interval Membership under Subtraction: Left Version

Informal description

For elements $a, b, c, d$ in an ordered additive monoid $\alpha$, the difference $a - b$ lies in the open interval $(c, d)$ if and only if $a$ lies in the open interval $(c + b, d + b)$. That is, \[ a - b \in (c, d) \iff a \in (c + b, d + b). \]

Set.sub_mem_Icc_iff_right theorem

: a - b ∈ Set.Icc c d ↔ b ∈ Set.Icc (a - d) (a - c)

Full source

theorem sub_mem_Icc_iff_right : a - b ∈ Set.Icc c da - b ∈ Set.Icc c d ↔ b ∈ Set.Icc (a - d) (a - c) :=
  and_comm.trans <| and_congr sub_le_comm le_sub_comm

Characterization of Subtraction in Closed Intervals

Informal description

For elements $a, b, c, d$ in an ordered additive monoid $\alpha$, the difference $a - b$ belongs to the closed interval $[c, d]$ if and only if $b$ belongs to the closed interval $[a - d, a - c]$. In other words: $$a - b \in [c, d] \iff b \in [a - d, a - c]$$

Set.sub_mem_Ico_iff_right theorem

: a - b ∈ Set.Ico c d ↔ b ∈ Set.Ioc (a - d) (a - c)

Full source

theorem sub_mem_Ico_iff_right : a - b ∈ Set.Ico c da - b ∈ Set.Ico c d ↔ b ∈ Set.Ioc (a - d) (a - c) :=
  and_comm.trans <| and_congr sub_lt_comm le_sub_comm

Characterization of Subtraction in Left-Closed Right-Open Intervals

Informal description

For elements $a, b, c, d$ in an ordered additive monoid $\alpha$, the difference $a - b$ belongs to the left-closed right-open interval $[c, d)$ if and only if $b$ belongs to the left-open right-closed interval $(a - d, a - c]$. In other words: $$a - b \in [c, d) \iff b \in (a - d, a - c]$$

Set.sub_mem_Ioc_iff_right theorem

: a - b ∈ Set.Ioc c d ↔ b ∈ Set.Ico (a - d) (a - c)

Full source

theorem sub_mem_Ioc_iff_right : a - b ∈ Set.Ioc c da - b ∈ Set.Ioc c d ↔ b ∈ Set.Ico (a - d) (a - c) :=
  and_comm.trans <| and_congr sub_le_comm lt_sub_comm

Characterization of Subtraction in Left-Open Right-Closed Intervals

Informal description

For elements $a, b, c, d$ in an ordered additive monoid $\alpha$, the difference $a - b$ belongs to the left-open right-closed interval $(c, d]$ if and only if $b$ belongs to the left-closed right-open interval $[a - d, a - c)$. In other words: $$a - b \in (c, d] \iff b \in [a - d, a - c)$$

Set.sub_mem_Ioo_iff_right theorem

: a - b ∈ Set.Ioo c d ↔ b ∈ Set.Ioo (a - d) (a - c)

Full source

theorem sub_mem_Ioo_iff_right : a - b ∈ Set.Ioo c da - b ∈ Set.Ioo c d ↔ b ∈ Set.Ioo (a - d) (a - c) :=
  and_comm.trans <| and_congr sub_lt_comm lt_sub_comm

Characterization of Subtraction in Open Intervals

Informal description

For any elements $a, b, c, d$ in an ordered additive monoid $\alpha$, the difference $a - b$ belongs to the open interval $(c, d)$ if and only if $b$ belongs to the open interval $(a - d, a - c)$. In other words: $$a - b \in (c, d) \iff b \in (a - d, a - c)$$

Set.mem_Icc_iff_abs_le theorem

 {R : Type*} [AddCommGroup R] [LinearOrder R] [IsOrderedAddMonoid R] {x y z : R} : |x - y| ≤ z ↔ y ∈ Icc (x - z) (x + z)

Full source

theorem mem_Icc_iff_abs_le {R : Type*}
    [AddCommGroup R] [LinearOrder R] [IsOrderedAddMonoid R] {x y z : R} :
    |x - y||x - y| ≤ z ↔ y ∈ Icc (x - z) (x + z) :=
  abs_le.trans <| and_comm.trans <| and_congr sub_le_comm neg_le_sub_iff_le_add

Characterization of Closed Interval via Absolute Difference

Informal description

Let $R$ be a linearly ordered additive commutative group. For any elements $x, y, z \in R$, the absolute difference $|x - y|$ is less than or equal to $z$ if and only if $y$ belongs to the closed interval $[x - z, x + z]$. In other words: $$|x - y| \leq z \iff y \in [x - z, x + z]$$

Set.sub_mem_Icc_zero_iff_right theorem

: b - a ∈ Icc 0 b ↔ a ∈ Icc 0 b

Full source

theorem sub_mem_Icc_zero_iff_right : b - a ∈ Icc 0 bb - a ∈ Icc 0 b ↔ a ∈ Icc 0 b := by
  simp only [sub_mem_Icc_iff_right, sub_self, sub_zero]

Difference in Closed Interval Zero to $b$ iff $a$ in Closed Interval Zero to $b$

Informal description

For any elements $a$ and $b$ in an ordered additive monoid, the difference $b - a$ belongs to the closed interval $[0, b]$ if and only if $a$ belongs to the closed interval $[0, b]$.

Set.sub_mem_Ico_zero_iff_right theorem

: b - a ∈ Ico 0 b ↔ a ∈ Ioc 0 b

Full source

theorem sub_mem_Ico_zero_iff_right : b - a ∈ Ico 0 bb - a ∈ Ico 0 b ↔ a ∈ Ioc 0 b := by
  simp only [sub_mem_Ico_iff_right, sub_self, sub_zero]

Difference in $[0, b)$ iff $a$ in $(0, b]$

Informal description

For any elements $a$ and $b$ in an ordered additive monoid, the difference $b - a$ belongs to the left-closed right-open interval $[0, b)$ if and only if $a$ belongs to the left-open right-closed interval $(0, b]$.

Set.sub_mem_Ioc_zero_iff_right theorem

: b - a ∈ Ioc 0 b ↔ a ∈ Ico 0 b

Full source

theorem sub_mem_Ioc_zero_iff_right : b - a ∈ Ioc 0 bb - a ∈ Ioc 0 b ↔ a ∈ Ico 0 b := by
  simp only [sub_mem_Ioc_iff_right, sub_self, sub_zero]

Difference in $(0, b]$ iff $a$ in $[0, b)$

Informal description

For any elements $a$ and $b$ in an ordered additive monoid, the difference $b - a$ belongs to the left-open right-closed interval $(0, b]$ if and only if $a$ belongs to the left-closed right-open interval $[0, b)$.

Set.sub_mem_Ioo_zero_iff_right theorem

: b - a ∈ Ioo 0 b ↔ a ∈ Ioo 0 b

Full source

theorem sub_mem_Ioo_zero_iff_right : b - a ∈ Ioo 0 bb - a ∈ Ioo 0 b ↔ a ∈ Ioo 0 b := by
  simp only [sub_mem_Ioo_iff_right, sub_self, sub_zero]

Difference in Open Interval Zero to $b$ iff $a$ in Open Interval Zero to $b$

Informal description

For any elements $a$ and $b$ in an ordered additive monoid $\alpha$, the difference $b - a$ belongs to the open interval $(0, b)$ if and only if $a$ belongs to the open interval $(0, b)$.

Set.nonempty_Ico_sdiff theorem

{x dx y dy : α} (h : dy < dx) (hx : 0 < dx) : Nonempty ↑(Ico x (x + dx) \ Ico y (y + dy))

Full source

/-- If we remove a smaller interval from a larger, the result is nonempty -/
theorem nonempty_Ico_sdiff {x dx y dy : α} (h : dy < dx) (hx : 0 < dx) :
    Nonempty ↑(IcoIco x (x + dx) \ Ico y (y + dy)) := by
  rcases lt_or_le x y with h' | h'
  · use x
    simp [*, not_le.2 h']
  · use max x (x + dy)
    simp [*, le_refl]

Nonemptiness of Interval Difference: $[x, x + dx) \setminus [y, y + dy)$ when $dy < dx$ and $dx > 0$

Informal description

For any elements $x, dx, y, dy$ in a linearly ordered additive monoid $\alpha$, if $dy < dx$ and $0 < dx$, then the set difference between the intervals $[x, x + dx)$ and $[y, y + dy)$ is nonempty.

Set.pairwise_disjoint_Ioc_mul_zpow theorem

: Pairwise (Disjoint on fun n : ℤ => Ioc (a * b ^ n) (a * b ^ (n + 1)))

Full source

@[to_additive]
theorem pairwise_disjoint_Ioc_mul_zpow :
    Pairwise (DisjointDisjoint on fun n : ℤ => Ioc (a * b ^ n) (a * b ^ (n + 1))) := by
  simp +unfoldPartialApp only [Function.onFun]
  simp_rw [Set.disjoint_iff]
  intro m n hmn x hx
  apply hmn
  have hb : 1 < b := by
    have : a * b ^ m < a * b ^ (m + 1) := hx.1.1.trans_le hx.1.2
    rwa [mul_lt_mul_iff_left, ← mul_one (b ^ m), zpow_add_one, mul_lt_mul_iff_left] at this
  have i1 := hx.1.1.trans_le hx.2.2
  have i2 := hx.2.1.trans_le hx.1.2
  rw [mul_lt_mul_iff_left, zpow_lt_zpow_iff_right hb, Int.lt_add_one_iff] at i1 i2
  exact le_antisymm i1 i2

Pairwise Disjointness of Scaled Power Intervals: $\left(a \cdot b^n, a \cdot b^{n+1}\right]$ for $n \in \mathbb{Z}$

Informal description

For any elements $a$ and $b$ in a linearly ordered additive monoid $\alpha$, the family of left-open right-closed intervals $\left(a \cdot b^n, a \cdot b^{n+1}\right]$ indexed by integers $n \in \mathbb{Z}$ is pairwise disjoint. That is, for any two distinct integers $n$ and $m$, the intervals $\left(a \cdot b^n, a \cdot b^{n+1}\right]$ and $\left(a \cdot b^m, a \cdot b^{m+1}\right]$ have no common elements.

Set.pairwise_disjoint_Ico_mul_zpow theorem

: Pairwise (Disjoint on fun n : ℤ => Ico (a * b ^ n) (a * b ^ (n + 1)))

Full source

@[to_additive]
theorem pairwise_disjoint_Ico_mul_zpow :
    Pairwise (DisjointDisjoint on fun n : ℤ => Ico (a * b ^ n) (a * b ^ (n + 1))) := by
  simp +unfoldPartialApp only [Function.onFun]
  simp_rw [Set.disjoint_iff]
  intro m n hmn x hx
  apply hmn
  have hb : 1 < b := by
    have : a * b ^ m < a * b ^ (m + 1) := hx.1.1.trans_lt hx.1.2
    rwa [mul_lt_mul_iff_left, ← mul_one (b ^ m), zpow_add_one, mul_lt_mul_iff_left] at this
  have i1 := hx.1.1.trans_lt hx.2.2
  have i2 := hx.2.1.trans_lt hx.1.2
  rw [mul_lt_mul_iff_left, zpow_lt_zpow_iff_right hb, Int.lt_add_one_iff] at i1 i2
  exact le_antisymm i1 i2

Pairwise Disjointness of Scaled Power Intervals $[a \cdot b^n, a \cdot b^{n+1})$ for $n \in \mathbb{Z}$

Informal description

For any elements $a$ and $b$ in a linearly ordered additive monoid $\alpha$, the family of left-closed right-open intervals $[a \cdot b^n, a \cdot b^{n+1})$ indexed by integers $n \in \mathbb{Z}$ is pairwise disjoint. That is, for any two distinct integers $m$ and $n$, the intervals $[a \cdot b^m, a \cdot b^{m+1})$ and $[a \cdot b^n, a \cdot b^{n+1})$ have empty intersection.

Set.pairwise_disjoint_Ioo_mul_zpow theorem

: Pairwise (Disjoint on fun n : ℤ => Ioo (a * b ^ n) (a * b ^ (n + 1)))

Full source

@[to_additive]
theorem pairwise_disjoint_Ioo_mul_zpow :
    Pairwise (DisjointDisjoint on fun n : ℤ => Ioo (a * b ^ n) (a * b ^ (n + 1))) := fun _ _ hmn =>
  (pairwise_disjoint_Ioc_mul_zpow a b hmn).mono Ioo_subset_Ioc_self Ioo_subset_Ioc_self

Pairwise Disjointness of Scaled Power Intervals: $\left(a \cdot b^n, a \cdot b^{n+1}\right)$ for $n \in \mathbb{Z}$

Informal description

For any elements $a$ and $b$ in a linearly ordered additive monoid $\alpha$, the family of open intervals $\left(a \cdot b^n, a \cdot b^{n+1}\right)$ indexed by integers $n \in \mathbb{Z}$ is pairwise disjoint. That is, for any two distinct integers $m$ and $n$, the intervals $\left(a \cdot b^m, a \cdot b^{m+1}\right)$ and $\left(a \cdot b^n, a \cdot b^{n+1}\right)$ have empty intersection.

Set.pairwise_disjoint_Ioc_zpow theorem

: Pairwise (Disjoint on fun n : ℤ => Ioc (b ^ n) (b ^ (n + 1)))

Full source

@[to_additive]
theorem pairwise_disjoint_Ioc_zpow :
    Pairwise (DisjointDisjoint on fun n : ℤ => Ioc (b ^ n) (b ^ (n + 1))) := by
  simpa only [one_mul] using pairwise_disjoint_Ioc_mul_zpow 1 b

Pairwise Disjointness of Power Intervals $\left(b^n, b^{n+1}\right]$ for $n \in \mathbb{Z}$

Informal description

For any element $b$ in a linearly ordered additive monoid $\alpha$, the family of left-open right-closed intervals $\left(b^n, b^{n+1}\right]$ indexed by integers $n \in \mathbb{Z}$ is pairwise disjoint. That is, for any two distinct integers $m$ and $n$, the intervals $\left(b^m, b^{m+1}\right]$ and $\left(b^n, b^{n+1}\right]$ have no common elements.

Set.pairwise_disjoint_Ico_zpow theorem

: Pairwise (Disjoint on fun n : ℤ => Ico (b ^ n) (b ^ (n + 1)))

Full source

@[to_additive]
theorem pairwise_disjoint_Ico_zpow :
    Pairwise (DisjointDisjoint on fun n : ℤ => Ico (b ^ n) (b ^ (n + 1))) := by
  simpa only [one_mul] using pairwise_disjoint_Ico_mul_zpow 1 b

Pairwise Disjointness of Power Intervals $[b^n, b^{n+1})$ for $n \in \mathbb{Z}$

Informal description

For any element $b$ in a linearly ordered additive monoid $\alpha$, the family of left-closed right-open intervals $[b^n, b^{n+1})$ indexed by integers $n \in \mathbb{Z}$ is pairwise disjoint. That is, for any two distinct integers $m$ and $n$, the intervals $[b^m, b^{m+1})$ and $[b^n, b^{n+1})$ have empty intersection.

Set.pairwise_disjoint_Ioo_zpow theorem

: Pairwise (Disjoint on fun n : ℤ => Ioo (b ^ n) (b ^ (n + 1)))

Full source

@[to_additive]
theorem pairwise_disjoint_Ioo_zpow :
    Pairwise (DisjointDisjoint on fun n : ℤ => Ioo (b ^ n) (b ^ (n + 1))) := by
  simpa only [one_mul] using pairwise_disjoint_Ioo_mul_zpow 1 b

Pairwise Disjointness of Power Intervals $\left(b^n, b^{n+1}\right)$ for $n \in \mathbb{Z}$

Informal description

For any element $b$ in a linearly ordered additive monoid $\alpha$, the family of open intervals $\left(b^n, b^{n+1}\right)$ indexed by integers $n \in \mathbb{Z}$ is pairwise disjoint. That is, for any two distinct integers $m$ and $n$, the intervals $\left(b^m, b^{m+1}\right)$ and $\left(b^n, b^{n+1}\right)$ have empty intersection.

Set.pairwise_disjoint_Ioc_add_intCast theorem

: Pairwise (Disjoint on fun n : ℤ => Ioc (a + n) (a + n + 1))

Full source

theorem pairwise_disjoint_Ioc_add_intCast :
    Pairwise (DisjointDisjoint on fun n : ℤ => Ioc (a + n) (a + n + 1)) := by
  simpa only [zsmul_one, Int.cast_add, Int.cast_one, ← add_assoc] using
    pairwise_disjoint_Ioc_add_zsmul a (1 : α)

Pairwise Disjointness of Translated Integer-Shifted Ioc Intervals

Informal description

For any real number $a$, the family of left-open right-closed intervals $\text{Ioc}(a + n, a + n + 1)$ indexed by integers $n \in \mathbb{Z}$ is pairwise disjoint. That is, for any two distinct integers $m$ and $n$, the intervals $\text{Ioc}(a + m, a + m + 1)$ and $\text{Ioc}(a + n, a + n + 1)$ have empty intersection.

Set.pairwise_disjoint_Ico_add_intCast theorem

: Pairwise (Disjoint on fun n : ℤ => Ico (a + n) (a + n + 1))

Full source

theorem pairwise_disjoint_Ico_add_intCast :
    Pairwise (DisjointDisjoint on fun n : ℤ => Ico (a + n) (a + n + 1)) := by
  simpa only [zsmul_one, Int.cast_add, Int.cast_one, ← add_assoc] using
    pairwise_disjoint_Ico_add_zsmul a (1 : α)

Pairwise Disjointness of Translated Unit Intervals: $\{[a + n, a + n + 1)\}_{n \in \mathbb{Z}}$

Informal description

For any real number $a$, the family of left-closed right-open intervals $\{[a + n, a + n + 1) \mid n \in \mathbb{Z}\}$ is pairwise disjoint. That is, for any two distinct integers $m$ and $n$, the intervals $[a + m, a + m + 1)$ and $[a + n, a + n + 1)$ have empty intersection.

Set.pairwise_disjoint_Ioo_add_intCast theorem

: Pairwise (Disjoint on fun n : ℤ => Ioo (a + n) (a + n + 1))

Full source

theorem pairwise_disjoint_Ioo_add_intCast :
    Pairwise (DisjointDisjoint on fun n : ℤ => Ioo (a + n) (a + n + 1)) := by
  simpa only [zsmul_one, Int.cast_add, Int.cast_one, ← add_assoc] using
    pairwise_disjoint_Ioo_add_zsmul a (1 : α)

Pairwise Disjointness of Translated Unit Open Intervals: $\{(a + n, a + n + 1)\}_{n \in \mathbb{Z}}$

Informal description

For any real number $a$, the family of open intervals $\{(a + n, a + n + 1) \mid n \in \mathbb{Z}\}$ is pairwise disjoint. That is, for any two distinct integers $m$ and $n$, the intervals $(a + m, a + m + 1)$ and $(a + n, a + n + 1)$ have empty intersection.

Set.pairwise_disjoint_Ico_intCast theorem

: Pairwise (Disjoint on fun n : ℤ => Ico (n : α) (n + 1))

Full source

theorem pairwise_disjoint_Ico_intCast :
    Pairwise (DisjointDisjoint on fun n : ℤ => Ico (n : α) (n + 1)) := by
  simpa only [zero_add] using pairwise_disjoint_Ico_add_intCast (0 : α)

Pairwise Disjointness of Integer-Translated Unit Intervals: $\{[n, n+1)\}_{n \in \mathbb{Z}}$

Informal description

For any ordered ring $\alpha$, the family of left-closed right-open intervals $\{[n, n+1) \mid n \in \mathbb{Z}\}$ is pairwise disjoint. That is, for any two distinct integers $m$ and $n$, the intervals $[m, m+1)$ and $[n, n+1)$ have empty intersection.

Set.pairwise_disjoint_Ioo_intCast theorem

: Pairwise (Disjoint on fun n : ℤ => Ioo (n : α) (n + 1))

Full source

theorem pairwise_disjoint_Ioo_intCast : Pairwise (DisjointDisjoint on fun n : ℤ => Ioo (n : α) (n + 1)) :=
  by simpa only [zero_add] using pairwise_disjoint_Ioo_add_intCast (0 : α)

Pairwise Disjointness of Integer-Translated Unit Open Intervals: $\{(n, n+1)\}_{n \in \mathbb{Z}}$

Informal description

For any ordered ring $\alpha$, the family of open intervals $\{(n, n+1) \mid n \in \mathbb{Z}\}$ is pairwise disjoint. That is, for any two distinct integers $m$ and $n$, the intervals $(m, m+1)$ and $(n, n+1)$ have empty intersection.

Set.pairwise_disjoint_Ioc_intCast theorem

: Pairwise (Disjoint on fun n : ℤ => Ioc (n : α) (n + 1))

Full source

theorem pairwise_disjoint_Ioc_intCast : Pairwise (DisjointDisjoint on fun n : ℤ => Ioc (n : α) (n + 1)) :=
  by simpa only [zero_add] using pairwise_disjoint_Ioc_add_intCast (0 : α)

Pairwise Disjointness of Integer-Shifted Ioc Intervals

Informal description

For any integer $n \in \mathbb{Z}$, the family of left-open right-closed intervals $\text{Ioc}(n, n + 1)$ is pairwise disjoint. That is, for any two distinct integers $m$ and $n$, the intervals $\text{Ioc}(m, m + 1)$ and $\text{Ioc}(n, n + 1)$ have empty intersection.