internlm/Lean-Github huggingface dataset:
Theorem: fourierConv_ofTwiceDifferentiable
Proof state before:
f : ℝ → ℂ
periodicf : Function.Periodic f (2 * Real.pi)
fdiff : ContDiff ℝ 2 f
ε : ℝ
εpos : ε > 0
fact_two_pi_pos : Fact (0 < 2 * Real.pi)
g : C(AddCircle (2 * Real.pi), ℂ) := { toFun := AddCircle.liftIco (2 * Real.pi) 0 f, continuous_toFun := ⋯ }
g_def : g = { toFun := AddCircle.liftIco (2 * Real.pi) 0 f, continuous_toFun := ⋯ }
two_pi_pos' : 0 < 0 + 2 * Real.pi
fourierCoeff_correspondence : ∀ {i : ℤ}, fourierCoeff (⇑g) i = fourierCoeffOn ⋯ f i
function_sum : HasSum (fun i => fourierCoeff (⇑g) i • fourier i) g
this✝ :
  ∀ ε > 0,
    ∀ᶠ (n : ℕ) in atTop,
      ∀ (x : AddCircle (2 * Real.pi)), dist (g x) ((∑ n ∈ Icc (-Int.ofNat n) ↑n, fourierCoeff (⇑g) n • fourier n) x) < ε
N₀ : ℕ
hN₀ :
  ∀ b ≥ N₀,
    ∀ (x : AddCircle (2 * Real.pi)), dist (g x) ((∑ n ∈ Icc (-Int.ofNat b) ↑b, fourierCoeff (⇑g) n • fourier n) x) < ε
N : ℕ
hN : N > N₀
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
this : Complex.abs (g ↑x - ∑ c ∈ Icc (-Int.ofNat N) ↑N, (fourierCoeff (⇑g) c • fourier c) ↑x) < ε
h : ¬x = 2 * Real.pi
⊢ x ∈ Set.Ico 0 (2 * Real.pi)
Tactic:
use hx.1
Proof state after:
case right
f : ℝ → ℂ
periodicf : Function.Periodic f (2 * Real.pi)
fdiff : ContDiff ℝ 2 f
ε : ℝ
εpos : ε > 0
fact_two_pi_pos : Fact (0 < 2 * Real.pi)
g : C(AddCircle (2 * Real.pi), ℂ) := { toFun := AddCircle.liftIco (2 * Real.pi) 0 f, continuous_toFun := ⋯ }
g_def : g = { toFun := AddCircle.liftIco (2 * Real.pi) 0 f, continuous_toFun := ⋯ }
two_pi_pos' : 0 < 0 + 2 * Real.pi
fourierCoeff_correspondence : ∀ {i : ℤ}, fourierCoeff (⇑g) i = fourierCoeffOn ⋯ f i
function_sum : HasSum (fun i => fourierCoeff (⇑g) i • fourier i) g
this✝ :
  ∀ ε > 0,
    ∀ᶠ (n : ℕ) in atTop,
      ∀ (x : AddCircle (2 * Real.pi)), dist (g x) ((∑ n ∈ Icc (-Int.ofNat n) ↑n, fourierCoeff (⇑g) n • fourier n) x) < ε
N₀ : ℕ
hN₀ :
  ∀ b ≥ N₀,
    ∀ (x : AddCircle (2 * Real.pi)), dist (g x) ((∑ n ∈ Icc (-Int.ofNat b) ↑b, fourierCoeff (⇑g) n • fourier n) x) < ε
N : ℕ
hN : N > N₀
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
this : Complex.abs (g ↑x - ∑ c ∈ Icc (-Int.ofNat N) ↑N, (fourierCoeff (⇑g) c • fourier c) ↑x) < ε
h : ¬x = 2 * Real.pi
⊢ x < 2 * Real.pi
Theorem: fourierConv_ofTwiceDifferentiable
Proof state before:
case right
f : ℝ → ℂ
periodicf : Function.Periodic f (2 * Real.pi)
fdiff : ContDiff ℝ 2 f
ε : ℝ
εpos : ε > 0
fact_two_pi_pos : Fact (0 < 2 * Real.pi)
g : C(AddCircle (2 * Real.pi), ℂ) := { toFun := AddCircle.liftIco (2 * Real.pi) 0 f, continuous_toFun := ⋯ }
g_def : g = { toFun := AddCircle.liftIco (2 * Real.pi) 0 f, continuous_toFun := ⋯ }
two_pi_pos' : 0 < 0 + 2 * Real.pi
fourierCoeff_correspondence : ∀ {i : ℤ}, fourierCoeff (⇑g) i = fourierCoeffOn ⋯ f i
function_sum : HasSum (fun i => fourierCoeff (⇑g) i • fourier i) g
this✝ :
  ∀ ε > 0,
    ∀ᶠ (n : ℕ) in atTop,
      ∀ (x : AddCircle (2 * Real.pi)), dist (g x) ((∑ n ∈ Icc (-Int.ofNat n) ↑n, fourierCoeff (⇑g) n • fourier n) x) < ε
N₀ : ℕ
hN₀ :
  ∀ b ≥ N₀,
    ∀ (x : AddCircle (2 * Real.pi)), dist (g x) ((∑ n ∈ Icc (-Int.ofNat b) ↑b, fourierCoeff (⇑g) n • fourier n) x) < ε
N : ℕ
hN : N > N₀
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
this : Complex.abs (g ↑x - ∑ c ∈ Icc (-Int.ofNat N) ↑N, (fourierCoeff (⇑g) c • fourier c) ↑x) < ε
h : ¬x = 2 * Real.pi
⊢ x < 2 * Real.pi
Tactic:
apply lt_of_le_of_ne hx.2 h
Proof state after:
no goals
Theorem: fourierConv_ofTwiceDifferentiable
Proof state before:
case h.e'_3.h.e'_6.e_a
f : ℝ → ℂ
periodicf : Function.Periodic f (2 * Real.pi)
fdiff : ContDiff ℝ 2 f
ε : ℝ
εpos : ε > 0
fact_two_pi_pos : Fact (0 < 2 * Real.pi)
g : C(AddCircle (2 * Real.pi), ℂ) := { toFun := AddCircle.liftIco (2 * Real.pi) 0 f, continuous_toFun := ⋯ }
g_def : g = { toFun := AddCircle.liftIco (2 * Real.pi) 0 f, continuous_toFun := ⋯ }
two_pi_pos' : 0 < 0 + 2 * Real.pi
fourierCoeff_correspondence : ∀ {i : ℤ}, fourierCoeff (⇑g) i = fourierCoeffOn ⋯ f i
function_sum : HasSum (fun i => fourierCoeff (⇑g) i • fourier i) g
this✝ :
  ∀ ε > 0,
    ∀ᶠ (n : ℕ) in atTop,
      ∀ (x : AddCircle (2 * Real.pi)), dist (g x) ((∑ n ∈ Icc (-Int.ofNat n) ↑n, fourierCoeff (⇑g) n • fourier n) x) < ε
N₀ : ℕ
hN₀ :
  ∀ b ≥ N₀,
    ∀ (x : AddCircle (2 * Real.pi)), dist (g x) ((∑ n ∈ Icc (-Int.ofNat b) ↑b, fourierCoeff (⇑g) n • fourier n) x) < ε
N : ℕ
hN : N > N₀
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
this : Complex.abs (g ↑x - ∑ c ∈ Icc (-Int.ofNat N) ↑N, (fourierCoeff (⇑g) c • fourier c) ↑x) < ε
⊢ partialFourierSum f N x = ∑ c ∈ Icc (-Int.ofNat N) ↑N, (fourierCoeff (⇑g) c • fourier c) ↑x
Tactic:
rw [partialFourierSum]
Proof state after:
case h.e'_3.h.e'_6.e_a
f : ℝ → ℂ
periodicf : Function.Periodic f (2 * Real.pi)
fdiff : ContDiff ℝ 2 f
ε : ℝ
εpos : ε > 0
fact_two_pi_pos : Fact (0 < 2 * Real.pi)
g : C(AddCircle (2 * Real.pi), ℂ) := { toFun := AddCircle.liftIco (2 * Real.pi) 0 f, continuous_toFun := ⋯ }
g_def : g = { toFun := AddCircle.liftIco (2 * Real.pi) 0 f, continuous_toFun := ⋯ }
two_pi_pos' : 0 < 0 + 2 * Real.pi
fourierCoeff_correspondence : ∀ {i : ℤ}, fourierCoeff (⇑g) i = fourierCoeffOn ⋯ f i
function_sum : HasSum (fun i => fourierCoeff (⇑g) i • fourier i) g
this✝ :
  ∀ ε > 0,
    ∀ᶠ (n : ℕ) in atTop,
      ∀ (x : AddCircle (2 * Real.pi)), dist (g x) ((∑ n ∈ Icc (-Int.ofNat n) ↑n, fourierCoeff (⇑g) n • fourier n) x) < ε
N₀ : ℕ
hN₀ :
  ∀ b ≥ N₀,
    ∀ (x : AddCircle (2 * Real.pi)), dist (g x) ((∑ n ∈ Icc (-Int.ofNat b) ↑b, fourierCoeff (⇑g) n • fourier n) x) < ε
N : ℕ
hN : N > N₀
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
this : Complex.abs (g ↑x - ∑ c ∈ Icc (-Int.ofNat N) ↑N, (fourierCoeff (⇑g) c • fourier c) ↑x) < ε
⊢ ∑ n ∈ Icc (-Int.ofNat N) ↑N, fourierCoeffOn Real.two_pi_pos f n * (fourier n) ↑x =
    ∑ c ∈ Icc (-Int.ofNat N) ↑N, (fourierCoeff (⇑g) c • fourier c) ↑x
Theorem: fourierConv_ofTwiceDifferentiable
Proof state before:
case h.e'_3.h.e'_6.e_a
f : ℝ → ℂ
periodicf : Function.Periodic f (2 * Real.pi)
fdiff : ContDiff ℝ 2 f
ε : ℝ
εpos : ε > 0
fact_two_pi_pos : Fact (0 < 2 * Real.pi)
g : C(AddCircle (2 * Real.pi), ℂ) := { toFun := AddCircle.liftIco (2 * Real.pi) 0 f, continuous_toFun := ⋯ }
g_def : g = { toFun := AddCircle.liftIco (2 * Real.pi) 0 f, continuous_toFun := ⋯ }
two_pi_pos' : 0 < 0 + 2 * Real.pi
fourierCoeff_correspondence : ∀ {i : ℤ}, fourierCoeff (⇑g) i = fourierCoeffOn ⋯ f i
function_sum : HasSum (fun i => fourierCoeff (⇑g) i • fourier i) g
this✝ :
  ∀ ε > 0,
    ∀ᶠ (n : ℕ) in atTop,
      ∀ (x : AddCircle (2 * Real.pi)), dist (g x) ((∑ n ∈ Icc (-Int.ofNat n) ↑n, fourierCoeff (⇑g) n • fourier n) x) < ε
N₀ : ℕ
hN₀ :
  ∀ b ≥ N₀,
    ∀ (x : AddCircle (2 * Real.pi)), dist (g x) ((∑ n ∈ Icc (-Int.ofNat b) ↑b, fourierCoeff (⇑g) n • fourier n) x) < ε
N : ℕ
hN : N > N₀
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
this : Complex.abs (g ↑x - ∑ c ∈ Icc (-Int.ofNat N) ↑N, (fourierCoeff (⇑g) c • fourier c) ↑x) < ε
⊢ ∑ n ∈ Icc (-Int.ofNat N) ↑N, fourierCoeffOn Real.two_pi_pos f n * (fourier n) ↑x =
    ∑ c ∈ Icc (-Int.ofNat N) ↑N, (fourierCoeff (⇑g) c • fourier c) ↑x
Tactic:
congr
Proof state after:
case h.e'_3.h.e'_6.e_a.e_f
f : ℝ → ℂ
periodicf : Function.Periodic f (2 * Real.pi)
fdiff : ContDiff ℝ 2 f
ε : ℝ
εpos : ε > 0
fact_two_pi_pos : Fact (0 < 2 * Real.pi)
g : C(AddCircle (2 * Real.pi), ℂ) := { toFun := AddCircle.liftIco (2 * Real.pi) 0 f, continuous_toFun := ⋯ }
g_def : g = { toFun := AddCircle.liftIco (2 * Real.pi) 0 f, continuous_toFun := ⋯ }
two_pi_pos' : 0 < 0 + 2 * Real.pi
fourierCoeff_correspondence : ∀ {i : ℤ}, fourierCoeff (⇑g) i = fourierCoeffOn ⋯ f i
function_sum : HasSum (fun i => fourierCoeff (⇑g) i • fourier i) g
this✝ :
  ∀ ε > 0,
    ∀ᶠ (n : ℕ) in atTop,
      ∀ (x : AddCircle (2 * Real.pi)), dist (g x) ((∑ n ∈ Icc (-Int.ofNat n) ↑n, fourierCoeff (⇑g) n • fourier n) x) < ε
N₀ : ℕ
hN₀ :
  ∀ b ≥ N₀,
    ∀ (x : AddCircle (2 * Real.pi)), dist (g x) ((∑ n ∈ Icc (-Int.ofNat b) ↑b, fourierCoeff (⇑g) n • fourier n) x) < ε
N : ℕ
hN : N > N₀
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
this : Complex.abs (g ↑x - ∑ c ∈ Icc (-Int.ofNat N) ↑N, (fourierCoeff (⇑g) c • fourier c) ↑x) < ε
⊢ (fun n => fourierCoeffOn Real.two_pi_pos f n * (fourier n) ↑x) = fun c => (fourierCoeff (⇑g) c • fourier c) ↑x
Theorem: fourierConv_ofTwiceDifferentiable
Proof state before:
case h.e'_3.h.e'_6.e_a.e_f
f : ℝ → ℂ
periodicf : Function.Periodic f (2 * Real.pi)
fdiff : ContDiff ℝ 2 f
ε : ℝ
εpos : ε > 0
fact_two_pi_pos : Fact (0 < 2 * Real.pi)
g : C(AddCircle (2 * Real.pi), ℂ) := { toFun := AddCircle.liftIco (2 * Real.pi) 0 f, continuous_toFun := ⋯ }
g_def : g = { toFun := AddCircle.liftIco (2 * Real.pi) 0 f, continuous_toFun := ⋯ }
two_pi_pos' : 0 < 0 + 2 * Real.pi
fourierCoeff_correspondence : ∀ {i : ℤ}, fourierCoeff (⇑g) i = fourierCoeffOn ⋯ f i
function_sum : HasSum (fun i => fourierCoeff (⇑g) i • fourier i) g
this✝ :
  ∀ ε > 0,
    ∀ᶠ (n : ℕ) in atTop,
      ∀ (x : AddCircle (2 * Real.pi)), dist (g x) ((∑ n ∈ Icc (-Int.ofNat n) ↑n, fourierCoeff (⇑g) n • fourier n) x) < ε
N₀ : ℕ
hN₀ :
  ∀ b ≥ N₀,
    ∀ (x : AddCircle (2 * Real.pi)), dist (g x) ((∑ n ∈ Icc (-Int.ofNat b) ↑b, fourierCoeff (⇑g) n • fourier n) x) < ε
N : ℕ
hN : N > N₀
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
this : Complex.abs (g ↑x - ∑ c ∈ Icc (-Int.ofNat N) ↑N, (fourierCoeff (⇑g) c • fourier c) ↑x) < ε
⊢ (fun n => fourierCoeffOn Real.two_pi_pos f n * (fourier n) ↑x) = fun c => (fourierCoeff (⇑g) c • fourier c) ↑x
Tactic:
ext n
Proof state after:
case h.e'_3.h.e'_6.e_a.e_f.h
f : ℝ → ℂ
periodicf : Function.Periodic f (2 * Real.pi)
fdiff : ContDiff ℝ 2 f
ε : ℝ
εpos : ε > 0
fact_two_pi_pos : Fact (0 < 2 * Real.pi)
g : C(AddCircle (2 * Real.pi), ℂ) := { toFun := AddCircle.liftIco (2 * Real.pi) 0 f, continuous_toFun := ⋯ }
g_def : g = { toFun := AddCircle.liftIco (2 * Real.pi) 0 f, continuous_toFun := ⋯ }
two_pi_pos' : 0 < 0 + 2 * Real.pi
fourierCoeff_correspondence : ∀ {i : ℤ}, fourierCoeff (⇑g) i = fourierCoeffOn ⋯ f i
function_sum : HasSum (fun i => fourierCoeff (⇑g) i • fourier i) g
this✝ :
  ∀ ε > 0,
    ∀ᶠ (n : ℕ) in atTop,
      ∀ (x : AddCircle (2 * Real.pi)), dist (g x) ((∑ n ∈ Icc (-Int.ofNat n) ↑n, fourierCoeff (⇑g) n • fourier n) x) < ε
N₀ : ℕ
hN₀ :
  ∀ b ≥ N₀,
    ∀ (x : AddCircle (2 * Real.pi)), dist (g x) ((∑ n ∈ Icc (-Int.ofNat b) ↑b, fourierCoeff (⇑g) n • fourier n) x) < ε
N : ℕ
hN : N > N₀
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
this : Complex.abs (g ↑x - ∑ c ∈ Icc (-Int.ofNat N) ↑N, (fourierCoeff (⇑g) c • fourier c) ↑x) < ε
n : ℤ
⊢ fourierCoeffOn Real.two_pi_pos f n * (fourier n) ↑x = (fourierCoeff (⇑g) n • fourier n) ↑x
Theorem: fourierConv_ofTwiceDifferentiable
Proof state before:
case h.e'_3.h.e'_6.e_a.e_f.h
f : ℝ → ℂ
periodicf : Function.Periodic f (2 * Real.pi)
fdiff : ContDiff ℝ 2 f
ε : ℝ
εpos : ε > 0
fact_two_pi_pos : Fact (0 < 2 * Real.pi)
g : C(AddCircle (2 * Real.pi), ℂ) := { toFun := AddCircle.liftIco (2 * Real.pi) 0 f, continuous_toFun := ⋯ }
g_def : g = { toFun := AddCircle.liftIco (2 * Real.pi) 0 f, continuous_toFun := ⋯ }
two_pi_pos' : 0 < 0 + 2 * Real.pi
fourierCoeff_correspondence : ∀ {i : ℤ}, fourierCoeff (⇑g) i = fourierCoeffOn ⋯ f i
function_sum : HasSum (fun i => fourierCoeff (⇑g) i • fourier i) g
this✝ :
  ∀ ε > 0,
    ∀ᶠ (n : ℕ) in atTop,
      ∀ (x : AddCircle (2 * Real.pi)), dist (g x) ((∑ n ∈ Icc (-Int.ofNat n) ↑n, fourierCoeff (⇑g) n • fourier n) x) < ε
N₀ : ℕ
hN₀ :
  ∀ b ≥ N₀,
    ∀ (x : AddCircle (2 * Real.pi)), dist (g x) ((∑ n ∈ Icc (-Int.ofNat b) ↑b, fourierCoeff (⇑g) n • fourier n) x) < ε
N : ℕ
hN : N > N₀
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
this : Complex.abs (g ↑x - ∑ c ∈ Icc (-Int.ofNat N) ↑N, (fourierCoeff (⇑g) c • fourier c) ↑x) < ε
n : ℤ
⊢ fourierCoeffOn Real.two_pi_pos f n * (fourier n) ↑x = (fourierCoeff (⇑g) n • fourier n) ↑x
Tactic:
rw [fourierCoeff_correspondence]
Proof state after:
case h.e'_3.h.e'_6.e_a.e_f.h
f : ℝ → ℂ
periodicf : Function.Periodic f (2 * Real.pi)
fdiff : ContDiff ℝ 2 f
ε : ℝ
εpos : ε > 0
fact_two_pi_pos : Fact (0 < 2 * Real.pi)
g : C(AddCircle (2 * Real.pi), ℂ) := { toFun := AddCircle.liftIco (2 * Real.pi) 0 f, continuous_toFun := ⋯ }
g_def : g = { toFun := AddCircle.liftIco (2 * Real.pi) 0 f, continuous_toFun := ⋯ }
two_pi_pos' : 0 < 0 + 2 * Real.pi
fourierCoeff_correspondence : ∀ {i : ℤ}, fourierCoeff (⇑g) i = fourierCoeffOn ⋯ f i
function_sum : HasSum (fun i => fourierCoeff (⇑g) i • fourier i) g
this✝ :
  ∀ ε > 0,
    ∀ᶠ (n : ℕ) in atTop,
      ∀ (x : AddCircle (2 * Real.pi)), dist (g x) ((∑ n ∈ Icc (-Int.ofNat n) ↑n, fourierCoeff (⇑g) n • fourier n) x) < ε
N₀ : ℕ
hN₀ :
  ∀ b ≥ N₀,
    ∀ (x : AddCircle (2 * Real.pi)), dist (g x) ((∑ n ∈ Icc (-Int.ofNat b) ↑b, fourierCoeff (⇑g) n • fourier n) x) < ε
N : ℕ
hN : N > N₀
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
this : Complex.abs (g ↑x - ∑ c ∈ Icc (-Int.ofNat N) ↑N, (fourierCoeff (⇑g) c • fourier c) ↑x) < ε
n : ℤ
⊢ fourierCoeffOn Real.two_pi_pos f n * (fourier n) ↑x = (fourierCoeffOn ⋯ f n • fourier n) ↑x
Theorem: fourierConv_ofTwiceDifferentiable
Proof state before:
case h.e'_3.h.e'_6.e_a.e_f.h
f : ℝ → ℂ
periodicf : Function.Periodic f (2 * Real.pi)
fdiff : ContDiff ℝ 2 f
ε : ℝ
εpos : ε > 0
fact_two_pi_pos : Fact (0 < 2 * Real.pi)
g : C(AddCircle (2 * Real.pi), ℂ) := { toFun := AddCircle.liftIco (2 * Real.pi) 0 f, continuous_toFun := ⋯ }
g_def : g = { toFun := AddCircle.liftIco (2 * Real.pi) 0 f, continuous_toFun := ⋯ }
two_pi_pos' : 0 < 0 + 2 * Real.pi
fourierCoeff_correspondence : ∀ {i : ℤ}, fourierCoeff (⇑g) i = fourierCoeffOn ⋯ f i
function_sum : HasSum (fun i => fourierCoeff (⇑g) i • fourier i) g
this✝ :
  ∀ ε > 0,
    ∀ᶠ (n : ℕ) in atTop,
      ∀ (x : AddCircle (2 * Real.pi)), dist (g x) ((∑ n ∈ Icc (-Int.ofNat n) ↑n, fourierCoeff (⇑g) n • fourier n) x) < ε
N₀ : ℕ
hN₀ :
  ∀ b ≥ N₀,
    ∀ (x : AddCircle (2 * Real.pi)), dist (g x) ((∑ n ∈ Icc (-Int.ofNat b) ↑b, fourierCoeff (⇑g) n • fourier n) x) < ε
N : ℕ
hN : N > N₀
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
this : Complex.abs (g ↑x - ∑ c ∈ Icc (-Int.ofNat N) ↑N, (fourierCoeff (⇑g) c • fourier c) ↑x) < ε
n : ℤ
⊢ fourierCoeffOn Real.two_pi_pos f n * (fourier n) ↑x = (fourierCoeffOn ⋯ f n • fourier n) ↑x
Tactic:
simp
Proof state after:
no goals
Theorem: CoveredByBalls.mono_set
Proof state before:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r r' r₁ r₂ r₃ : ℝ
h : CoveredByBalls t n r
h2 : s ⊆ t
⊢ CoveredByBalls s n r
Tactic:
induction h
Proof state after:
case mk
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r r' r₁ r₂ r₃ : ℝ
h2 : s ⊆ t
balls✝ : Finset X
card_balls✝ : balls✝.card ≤ n
union_balls✝ : t ⊆ ⋃ x ∈ balls✝, ball x r
⊢ CoveredByBalls s n r
Theorem: CoveredByBalls.mono_set
Proof state before:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r r' r₁ r₂ r₃ : ℝ
h2 : s ⊆ t
b : Finset X
hn : b.card ≤ n
ht : t ⊆ ⋃ x ∈ b, ball x r
⊢ CoveredByBalls s n r
Tactic:
case mk b hn ht =>
  exact ⟨b, hn, fun x hx ↦ ht (h2 hx)⟩
Proof state after:
no goals
Theorem: CoveredByBalls.mono_set
Proof state before:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r r' r₁ r₂ r₃ : ℝ
h2 : s ⊆ t
b : Finset X
hn : b.card ≤ n
ht : t ⊆ ⋃ x ∈ b, ball x r
⊢ CoveredByBalls s n r
Tactic:
exact ⟨b, hn, fun x hx ↦ ht (h2 hx)⟩
Proof state after:
no goals
Theorem: CoveredByBalls.mono_nat
Proof state before:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r r' r₁ r₂ r₃ : ℝ
h : CoveredByBalls s n r
h2 : n ≤ m
⊢ CoveredByBalls s m r
Tactic:
induction h
Proof state after:
case mk
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r r' r₁ r₂ r₃ : ℝ
h2 : n ≤ m
balls✝ : Finset X
card_balls✝ : balls✝.card ≤ n
union_balls✝ : s ⊆ ⋃ x ∈ balls✝, ball x r
⊢ CoveredByBalls s m r
Theorem: CoveredByBalls.mono_nat
Proof state before:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r r' r₁ r₂ r₃ : ℝ
h2 : n ≤ m
b : Finset X
hn : b.card ≤ n
hs : s ⊆ ⋃ x ∈ b, ball x r
⊢ CoveredByBalls s m r
Tactic:
case mk b hn hs =>
  exact ⟨b, hn.trans h2, hs⟩
Proof state after:
no goals
Theorem: CoveredByBalls.mono_nat
Proof state before:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r r' r₁ r₂ r₃ : ℝ
h2 : n ≤ m
b : Finset X
hn : b.card ≤ n
hs : s ⊆ ⋃ x ∈ b, ball x r
⊢ CoveredByBalls s m r
Tactic:
exact ⟨b, hn.trans h2, hs⟩
Proof state after:
no goals
Theorem: CoveredByBalls.mono_real
Proof state before:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r r' r₁ r₂ r₃ : ℝ
h : CoveredByBalls s n r
h2 : r ≤ r'
⊢ CoveredByBalls s n r'
Tactic:
induction h
Proof state after:
case mk
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r r' r₁ r₂ r₃ : ℝ
h2 : r ≤ r'
balls✝ : Finset X
card_balls✝ : balls✝.card ≤ n
union_balls✝ : s ⊆ ⋃ x ∈ balls✝, ball x r
⊢ CoveredByBalls s n r'
Theorem: CoveredByBalls.mono_real
Proof state before:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r r' r₁ r₂ r₃ : ℝ
h2 : r ≤ r'
b : Finset X
hn : b.card ≤ n
hs : s ⊆ ⋃ x ∈ b, ball x r
⊢ CoveredByBalls s n r'
Tactic:
case mk b hn hs =>
  exact ⟨b, hn, hs.trans (by gcongr)⟩
Proof state after:
no goals
Theorem: CoveredByBalls.mono_real
Proof state before:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r r' r₁ r₂ r₃ : ℝ
h2 : r ≤ r'
b : Finset X
hn : b.card ≤ n
hs : s ⊆ ⋃ x ∈ b, ball x r
⊢ CoveredByBalls s n r'
Tactic:
exact ⟨b, hn, hs.trans (by gcongr)⟩
Proof state after:
no goals
Theorem: CoveredByBalls.mono_real
Proof state before:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r r' r₁ r₂ r₃ : ℝ
h2 : r ≤ r'
b : Finset X
hn : b.card ≤ n
hs : s ⊆ ⋃ x ∈ b, ball x r
⊢ ⋃ x ∈ b, ball x r ⊆ ⋃ x ∈ b, ball x r'
Tactic:
gcongr
Proof state after:
no goals
Theorem: CoveredByBalls.empty
Proof state before:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r r' r₁ r₂ r₃ : ℝ
⊢ ∅.card ≤ n
Tactic:
simp
Proof state after:
no goals
Theorem: CoveredByBalls.empty
Proof state before:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r r' r₁ r₂ r₃ : ℝ
⊢ ∅ ⊆ ⋃ x ∈ ∅, ball x r
Tactic:
simp
Proof state after:
no goals
Theorem: CoveredByBalls.zero_left
Proof state before:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r r' r₁ r₂ r₃ : ℝ
⊢ CoveredByBalls s 0 r ↔ s = ∅
Tactic:
have h1 : CoveredByBalls s 0 r → s = ∅ := by
  intro ⟨b, hn, hs⟩
  simp at hn
  subst hn
  simp at hs
  exact Set.subset_eq_empty hs rfl
Proof state after:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r r' r₁ r₂ r₃ : ℝ
h1 : CoveredByBalls s 0 r → s = ∅
⊢ CoveredByBalls s 0 r ↔ s = ∅
Theorem: CoveredByBalls.zero_left
Proof state before:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r r' r₁ r₂ r₃ : ℝ
h1 : CoveredByBalls s 0 r → s = ∅
⊢ CoveredByBalls s 0 r ↔ s = ∅
Tactic:
have h2 : s = ∅ → CoveredByBalls s 0 r := by
  rintro rfl
  exact CoveredByBalls.empty
Proof state after:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r r' r₁ r₂ r₃ : ℝ
h1 : CoveredByBalls s 0 r → s = ∅
h2 : s = ∅ → CoveredByBalls s 0 r
⊢ CoveredByBalls s 0 r ↔ s = ∅
Theorem: CoveredByBalls.zero_left
Proof state before:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r r' r₁ r₂ r₃ : ℝ
h1 : CoveredByBalls s 0 r → s = ∅
h2 : s = ∅ → CoveredByBalls s 0 r
⊢ CoveredByBalls s 0 r ↔ s = ∅
Tactic:
exact { mp := h1, mpr := h2 }
Proof state after:
no goals
Theorem: CoveredByBalls.zero_left
Proof state before:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r r' r₁ r₂ r₃ : ℝ
⊢ CoveredByBalls s 0 r → s = ∅
Tactic:
intro ⟨b, hn, hs⟩
Proof state after:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r r' r₁ r₂ r₃ : ℝ
b : Finset X
hn : b.card ≤ 0
hs : s ⊆ ⋃ x ∈ b, ball x r
⊢ s = ∅
Theorem: CoveredByBalls.zero_left
Proof state before:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r r' r₁ r₂ r₃ : ℝ
b : Finset X
hn : b.card ≤ 0
hs : s ⊆ ⋃ x ∈ b, ball x r
⊢ s = ∅
Tactic:
simp at hn
Proof state after:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r r' r₁ r₂ r₃ : ℝ
b : Finset X
hs : s ⊆ ⋃ x ∈ b, ball x r
hn : b = ∅
⊢ s = ∅
Theorem: CoveredByBalls.zero_left
Proof state before:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r r' r₁ r₂ r₃ : ℝ
b : Finset X
hs : s ⊆ ⋃ x ∈ b, ball x r
hn : b = ∅
⊢ s = ∅
Tactic:
subst hn
Proof state after:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r r' r₁ r₂ r₃ : ℝ
hs : s ⊆ ⋃ x ∈ ∅, ball x r
⊢ s = ∅
Theorem: CoveredByBalls.zero_left
Proof state before:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r r' r₁ r₂ r₃ : ℝ
hs : s ⊆ ⋃ x ∈ ∅, ball x r
⊢ s = ∅
Tactic:
simp at hs
Proof state after:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r r' r₁ r₂ r₃ : ℝ
hs : s ⊆ ∅
⊢ s = ∅
Theorem: CoveredByBalls.zero_left
Proof state before:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r r' r₁ r₂ r₃ : ℝ
hs : s ⊆ ∅
⊢ s = ∅
Tactic:
exact Set.subset_eq_empty hs rfl
Proof state after:
no goals
Theorem: CoveredByBalls.zero_left
Proof state before:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r r' r₁ r₂ r₃ : ℝ
h1 : CoveredByBalls s 0 r → s = ∅
⊢ s = ∅ → CoveredByBalls s 0 r
Tactic:
rintro rfl
Proof state after:
X : Type u_1
inst✝ : PseudoMetricSpace X
t : Set X
n m : ℕ
r r' r₁ r₂ r₃ : ℝ
h1 : CoveredByBalls ∅ 0 r → ∅ = ∅
⊢ CoveredByBalls ∅ 0 r
Theorem: CoveredByBalls.zero_left
Proof state before:
X : Type u_1
inst✝ : PseudoMetricSpace X
t : Set X
n m : ℕ
r r' r₁ r₂ r₃ : ℝ
h1 : CoveredByBalls ∅ 0 r → ∅ = ∅
⊢ CoveredByBalls ∅ 0 r
Tactic:
exact CoveredByBalls.empty
Proof state after:
no goals
Theorem: CoveredByBalls.zero_right
Proof state before:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r r' r₁ r₂ r₃ : ℝ
⊢ CoveredByBalls s n 0 ↔ s = ∅
Tactic:
have h1 : CoveredByBalls s n 0 → s =∅ := by
  intro hcovered
  cases hcovered
  case mk b hn hs =>
  simp at hs
  exact Set.subset_eq_empty hs rfl
Proof state after:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r r' r₁ r₂ r₃ : ℝ
h1 : CoveredByBalls s n 0 → s = ∅
⊢ CoveredByBalls s n 0 ↔ s = ∅
Theorem: CoveredByBalls.zero_right
Proof state before:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r r' r₁ r₂ r₃ : ℝ
h1 : CoveredByBalls s n 0 → s = ∅
⊢ CoveredByBalls s n 0 ↔ s = ∅
Tactic:
have h2 : s = ∅ → CoveredByBalls s n 0 := by
  intro hs
  have h21 : (∅ : Finset X).card ≤ n := by exact tsub_add_cancel_iff_le.mp rfl
  have h22 : s ⊆ ⋃ x ∈ (∅ : Finset X), ball x 0 := by
    simp only [not_mem_empty, ball_zero, Set.iUnion_of_empty, Set.iUnion_empty]
    exact Set.subset_empty_iff.mpr hs
  exact ⟨(∅ : Finset X), h21, h22⟩
Proof state after:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r r' r₁ r₂ r₃ : ℝ
h1 : CoveredByBalls s n 0 → s = ∅
h2 : s = ∅ → CoveredByBalls s n 0
⊢ CoveredByBalls s n 0 ↔ s = ∅
Theorem: CoveredByBalls.zero_right
Proof state before:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r r' r₁ r₂ r₃ : ℝ
h1 : CoveredByBalls s n 0 → s = ∅
h2 : s = ∅ → CoveredByBalls s n 0
⊢ CoveredByBalls s n 0 ↔ s = ∅
Tactic:
exact { mp := h1, mpr := h2 }
Proof state after:
no goals
Theorem: CoveredByBalls.zero_right
Proof state before:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r r' r₁ r₂ r₃ : ℝ
⊢ CoveredByBalls s n 0 → s = ∅
Tactic:
intro hcovered
Proof state after:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r r' r₁ r₂ r₃ : ℝ
hcovered : CoveredByBalls s n 0
⊢ s = ∅
Theorem: CoveredByBalls.zero_right
Proof state before:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r r' r₁ r₂ r₃ : ℝ
hcovered : CoveredByBalls s n 0
⊢ s = ∅
Tactic:
cases hcovered
Proof state after:
case mk
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r r' r₁ r₂ r₃ : ℝ
balls✝ : Finset X
card_balls✝ : balls✝.card ≤ n
union_balls✝ : s ⊆ ⋃ x ∈ balls✝, ball x 0
⊢ s = ∅
Theorem: CoveredByBalls.zero_right
Proof state before:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r r' r₁ r₂ r₃ : ℝ
b : Finset X
hn : b.card ≤ n
hs : s ⊆ ⋃ x ∈ b, ball x 0
⊢ s = ∅
Tactic:
case mk b hn hs =>
simp at hs
exact Set.subset_eq_empty hs rfl
Proof state after:
no goals
Theorem: CoveredByBalls.zero_right
Proof state before:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r r' r₁ r₂ r₃ : ℝ
b : Finset X
hn : b.card ≤ n
hs : s ⊆ ⋃ x ∈ b, ball x 0
⊢ s = ∅
Tactic:
simp at hs
Proof state after:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r r' r₁ r₂ r₃ : ℝ
b : Finset X
hn : b.card ≤ n
hs : s ⊆ ∅
⊢ s = ∅
Theorem: CoveredByBalls.zero_right
Proof state before:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r r' r₁ r₂ r₃ : ℝ
b : Finset X
hn : b.card ≤ n
hs : s ⊆ ∅
⊢ s = ∅
Tactic:
exact Set.subset_eq_empty hs rfl
Proof state after:
no goals