ℝ lemmas

theorem mem_if_univ_iff {α : Type} {x : α} {u : Set α} {p : Prop} {dp : Decidable p} : (x ∈ if p then Set.univ else u) ↔ ¬p → x ∈ u

Simplify to case assuming not nan

theorem subset_if_univ_iff {α : Type} {t u : Set α} {p : Prop} {dp : Decidable p} : (t ⊆ if p then Set.univ else u) ↔ ¬p → t ⊆ u

Simplify to case assuming not nan

theorem nonpos_or_nonneg {𝕜 : Type} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] (x : 𝕜) : x ≤ 0 ∨ 0 ≤ x

Reals are either ≤ 0 or ≥ 0

@[simp]

theorem range_mul_right_eq_univ {𝕝 : Type} [Field 𝕝] {a : 𝕝} (a0 : a ≠ 0) : (Set.range fun (x : 𝕝) => x * a) = Set.univ

The range of nonzero multiplication is univ

@[simp]

theorem Set.univ_mul_singleton {𝕝 : Type} [Field 𝕝] {a : 𝕝} (a0 : a ≠ 0) : univ * {a} = univ

Multiplying by a nonzero preserves univ

@[simp]

theorem Set.Icc_mul_singleton {𝕜 : Type} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {a b x : 𝕜} (x0 : 0 < x) : Icc a b * {x} = Icc (a * x) (b * x)

Multiplying an Icc by a positive number produces the expected Icc

theorem image_mul_right_Icc_of_neg {𝕜 : Type} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {a b c : 𝕜} (c0 : c < 0) : (fun (x : 𝕜) => x * c) '' Set.Icc a b = Set.Icc (b * c) (a * c)

Negative c version of image_mul_right_Icc

@[simp]

theorem two_pow_pos {R : Type} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] {n : ℕ} : 0 < 2 ^ n

A simple lemma that we use a lot

@[simp]

theorem two_zpow_pos {𝕜 : Type} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {n : ℤ} : 0 < 2 ^ n

A simple lemma that we use a lot

@[simp]

theorem two_zpow_not_nonpos {𝕜 : Type} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {n : ℤ} : ¬2 ^ n ≤ 0

Writing not_lt.mpr two_zpow_pos fails to infer inside simp, so we write this out

@[simp]

theorem two_zpow_not_neg {𝕜 : Type} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {n : ℤ} : ¬2 ^ n < 0

Writing not_lt.mpr two_zpow_pos.le fails to infer inside simp, so we write this out

@[simp]

theorem range_mul_two_zpow_eq_univ {𝕜 : Type} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {n : ℤ} : (Set.range fun (x : 𝕜) => x * 2 ^ n) = Set.univ

The range of two power multiplication is univ

@[simp]

theorem Set.Icc_mul_two_zpow {𝕜 : Type} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {a b : 𝕜} {n : ℤ} : Icc a b * {2 ^ n} = Icc (a * 2 ^ n) (b * 2 ^ n)

Multiplying an Icc by a two power is nice

theorem Set.inv_Icc₀ {𝕜 : Type} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {a b : 𝕜} (a0 : 0 < a) (b0 : 0 < b) : (Icc a b)⁻¹ = Icc b⁻¹ a⁻¹

Icc commutes with ⁻¹ if we're positive

theorem pow_mul_zpow {𝕝 : Type} [Field 𝕝] {a : 𝕝} (a0 : a ≠ 0) (b : ℕ) (c : ℤ) : a ^ b * a ^ c = a ^ (↑b + c)

pow and zpow multiply via addition

theorem zpow_mul_pow {𝕝 : Type} [Field 𝕝] {a : 𝕝} (a0 : a ≠ 0) (b : ℤ) (c : ℕ) : a ^ b * a ^ c = a ^ (b + ↑c)

zpow and pow divide via subtraction

theorem zpow_div_pow {𝕝 : Type} [Field 𝕝] {a : 𝕝} (a0 : a ≠ 0) (b : ℤ) (c : ℕ) : a ^ b / a ^ c = a ^ (b - ↑c)

pow and zpow multiply via addition

@[simp]

theorem Set.inv_neg {𝕝 : Type} [Field 𝕝] {s : Set 𝕝} : (-s)⁻¹ = -s⁻¹

- and ⁻¹ commute on Set ℝ

@[simp]

theorem sub_le_add_iff_left {𝕜 : Type} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] (x y z : 𝕜) : x - y ≤ x + z ↔ -y ≤ z

x - y ≤ x + z ↔ -y ≤ z

@[simp]

theorem add_le_sub_iff_left {𝕜 : Type} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] (x y z : 𝕜) : x + y ≤ x - z ↔ y ≤ -z

x + y ≤ x - z ↔ y ≤ -z

theorem Icc_mul_Icc_subset_Icc {a b c d x y : ℝ} (ab : a ≤ b) (cd : c ≤ d) : Set.Icc a b * Set.Icc c d ⊆ Set.Icc x y ↔ x ≤ a * c ∧ x ≤ a * d ∧ x ≤ b * c ∧ x ≤ b * d ∧ a * c ≤ y ∧ a * d ≤ y ∧ b * c ≤ y ∧ b * d ≤ y

Rewrite Icc * Icc ⊆ Icc in terms of inequalities

theorem sqr_Icc_subset_Icc {𝕜 : Type} [Field 𝕜] [LinearOrder 𝕜] {a b x y : 𝕜} : (fun (x : 𝕜) => x ^ 2) '' Set.Icc a b ⊆ Set.Icc x y ↔ ∀ (u : 𝕜), a ≤ u → u ≤ b → x ≤ u ^ 2 ∧ u ^ 2 ≤ y

Rewrite Icc^2 ⊆ Icc in terms of inequalities