LeanPool.Monsky.Miscellaneous

Imported Lean Pool material for LeanPool.Monsky.Miscellaneous.

theorem LeanPool.Monsky.sign_mul_pos {a b : ℝ} (ha : 0 < a) : (a * b).sign = b.sign

theorem LeanPool.Monsky.sign_pos' {a : ℝ} (h : a.sign = 1) : 0 < a

theorem LeanPool.Monsky.sign_neg' {a : ℝ} (h : a.sign = -1) : a < 0

theorem LeanPool.Monsky.sign_div_pos {a b : ℝ} (hb₀ : b ≠ 0) (hs : a.sign = b.sign) : 0 < a / b

theorem LeanPool.Monsky.real_sign_mul {x y : ℝ} : (x * y).sign = x.sign * y.sign

theorem LeanPool.Monsky.real_sign_involution {x : ℝ} : x.sign.sign = x.sign

theorem LeanPool.Monsky.real_sign_div_self {x : ℝ} (hx : x ≠ 0) : 0 < x.sign / x

theorem LeanPool.Monsky.real_sign_mul_self {x : ℝ} (hx : x ≠ 0) : 0 < x.sign * x

theorem LeanPool.Monsky.real_sign_abs_le {x : ℝ} : |x.sign| ≤ 1

theorem LeanPool.Monsky.mul_cancel {a b c : ℝ} (h : a ≠ 0) (h2 : a * b = a * c) : b = c

theorem LeanPool.Monsky.smul_cancel {a : ℝ} {b c : EuclideanSpace ℝ (Fin 2)} (h₁ : a ≠ 0) (h₂ : a • b = a • c) : b = c

theorem LeanPool.Monsky.fin2_im {α : Type} [DecidableEq α] {f : Fin 2 → α} : Finset.image f Finset.univ = {f 0, f 1}

theorem LeanPool.Monsky.forall_in_swap_special {α β : Type} {P : α → β → Prop} {Q : α → Prop} : (∀ (a : α), Q a → ∀ (b : β), P a b) ↔ ∀ (b : β) (a : α), Q a → P a b

theorem LeanPool.Monsky.forall_exists_pos_swap {α : Type} [Finite α] {P : ℝ → α → Prop} (h : ∀ (δ : ℝ) (a : α), P δ a → ∀ δ' ≤ δ, P δ' a) : (∃ δ > 0, ∀ (a : α), P δ a) ↔ ∀ (a : α), ∃ δ > 0, P δ a

theorem LeanPool.Monsky.real_interval_δ {x : ℝ} (y : ℝ) (hx : 0 < x) : ∃ δ > 0, ∀ (a : ℝ), |a| ≤ δ → 0 < x + a * y

For positive x, there is a radius δ > 0 within which x + a * y stays positive.

theorem LeanPool.Monsky.finset_infinite_pigeonhole {α β : Type} [Infinite α] {f : α → β} {B : Finset β} (hf : ∀ (a : α), f a ∈ B) : ∃ b ∈ B, (f ⁻¹' {b}).Infinite

theorem LeanPool.Monsky.infinite_distinct_el {α : Type} {S : Set α} (hS : S.Infinite) (k : α) : ∃ a ∈ S, a ≠ k

theorem LeanPool.Monsky.infinite_imp_two_distinct_el {α : Type} {S : Set α} (hS : S.Infinite) : ∃ a ∈ S, ∃ b ∈ S, a ≠ b