internlm/Lean-Github huggingface dataset:
Theorem: UniformCauchySeqOn.bounded
Proof state before:
case neg
X Y : Type
inst✝¹ : TopologicalSpace X
inst✝ : NormedAddCommGroup Y
f : ℕ → X → Y
s : Set X
fc : ∀ (n : ℕ), ContinuousOn (f n) s
sc : IsCompact s
c : ℕ → ℝ
hc : (fun n => Classical.choose ⋯) = c
cs : ∀ (n : ℕ), 0 ≤ c n ∧ ∀ x ∈ s, ‖f n x‖ ≤ c n
N : ℕ
H : ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ s, dist (f m x) (f n x) < 1
bs : Finset ℝ
hbs : Finset.image c (Finset.range (N + 1)) = bs
c0 : c 0 ∈ bs
b : ℝ
hb : 1 + bs.max' ⋯ = b
n : ℕ
x : X
xs : x ∈ s
nN : N < n
⊢ ‖f n x‖ ≤ b
Tactic:
specialize H N le_rfl n nN.le x xs
Proof state after:
case neg
X Y : Type
inst✝¹ : TopologicalSpace X
inst✝ : NormedAddCommGroup Y
f : ℕ → X → Y
s : Set X
fc : ∀ (n : ℕ), ContinuousOn (f n) s
sc : IsCompact s
c : ℕ → ℝ
hc : (fun n => Classical.choose ⋯) = c
cs : ∀ (n : ℕ), 0 ≤ c n ∧ ∀ x ∈ s, ‖f n x‖ ≤ c n
N : ℕ
bs : Finset ℝ
hbs : Finset.image c (Finset.range (N + 1)) = bs
c0 : c 0 ∈ bs
b : ℝ
hb : 1 + bs.max' ⋯ = b
n : ℕ
x : X
xs : x ∈ s
nN : N < n
H : dist (f N x) (f n x) < 1
⊢ ‖f n x‖ ≤ b
Theorem: UniformCauchySeqOn.bounded
Proof state before:
case neg
X Y : Type
inst✝¹ : TopologicalSpace X
inst✝ : NormedAddCommGroup Y
f : ℕ → X → Y
s : Set X
fc : ∀ (n : ℕ), ContinuousOn (f n) s
sc : IsCompact s
c : ℕ → ℝ
hc : (fun n => Classical.choose ⋯) = c
cs : ∀ (n : ℕ), 0 ≤ c n ∧ ∀ x ∈ s, ‖f n x‖ ≤ c n
N : ℕ
bs : Finset ℝ
hbs : Finset.image c (Finset.range (N + 1)) = bs
c0 : c 0 ∈ bs
b : ℝ
hb : 1 + bs.max' ⋯ = b
n : ℕ
x : X
xs : x ∈ s
nN : N < n
H : dist (f N x) (f n x) < 1
⊢ ‖f n x‖ ≤ b
Tactic:
have cN : c N ∈ bs := by simp [← hbs]; exists N; simp
Proof state after:
case neg
X Y : Type
inst✝¹ : TopologicalSpace X
inst✝ : NormedAddCommGroup Y
f : ℕ → X → Y
s : Set X
fc : ∀ (n : ℕ), ContinuousOn (f n) s
sc : IsCompact s
c : ℕ → ℝ
hc : (fun n => Classical.choose ⋯) = c
cs : ∀ (n : ℕ), 0 ≤ c n ∧ ∀ x ∈ s, ‖f n x‖ ≤ c n
N : ℕ
bs : Finset ℝ
hbs : Finset.image c (Finset.range (N + 1)) = bs
c0 : c 0 ∈ bs
b : ℝ
hb : 1 + bs.max' ⋯ = b
n : ℕ
x : X
xs : x ∈ s
nN : N < n
H : dist (f N x) (f n x) < 1
cN : c N ∈ bs
⊢ ‖f n x‖ ≤ b
Theorem: UniformCauchySeqOn.bounded
Proof state before:
case neg
X Y : Type
inst✝¹ : TopologicalSpace X
inst✝ : NormedAddCommGroup Y
f : ℕ → X → Y
s : Set X
fc : ∀ (n : ℕ), ContinuousOn (f n) s
sc : IsCompact s
c : ℕ → ℝ
hc : (fun n => Classical.choose ⋯) = c
cs : ∀ (n : ℕ), 0 ≤ c n ∧ ∀ x ∈ s, ‖f n x‖ ≤ c n
N : ℕ
bs : Finset ℝ
hbs : Finset.image c (Finset.range (N + 1)) = bs
c0 : c 0 ∈ bs
b : ℝ
hb : 1 + bs.max' ⋯ = b
n : ℕ
x : X
xs : x ∈ s
nN : N < n
H : dist (f N x) (f n x) < 1
cN : c N ∈ bs
⊢ ‖f n x‖ ≤ b
Tactic:
have bN := _root_.trans ((cs N).2 x xs) (Finset.le_max' _ _ cN)
Proof state after:
case neg
X Y : Type
inst✝¹ : TopologicalSpace X
inst✝ : NormedAddCommGroup Y
f : ℕ → X → Y
s : Set X
fc : ∀ (n : ℕ), ContinuousOn (f n) s
sc : IsCompact s
c : ℕ → ℝ
hc : (fun n => Classical.choose ⋯) = c
cs : ∀ (n : ℕ), 0 ≤ c n ∧ ∀ x ∈ s, ‖f n x‖ ≤ c n
N : ℕ
bs : Finset ℝ
hbs : Finset.image c (Finset.range (N + 1)) = bs
c0 : c 0 ∈ bs
b : ℝ
hb : 1 + bs.max' ⋯ = b
n : ℕ
x : X
xs : x ∈ s
nN : N < n
H : dist (f N x) (f n x) < 1
cN : c N ∈ bs
bN : ‖f N x‖ ≤ bs.max' ⋯
⊢ ‖f n x‖ ≤ b
Theorem: UniformCauchySeqOn.bounded
Proof state before:
case neg
X Y : Type
inst✝¹ : TopologicalSpace X
inst✝ : NormedAddCommGroup Y
f : ℕ → X → Y
s : Set X
fc : ∀ (n : ℕ), ContinuousOn (f n) s
sc : IsCompact s
c : ℕ → ℝ
hc : (fun n => Classical.choose ⋯) = c
cs : ∀ (n : ℕ), 0 ≤ c n ∧ ∀ x ∈ s, ‖f n x‖ ≤ c n
N : ℕ
bs : Finset ℝ
hbs : Finset.image c (Finset.range (N + 1)) = bs
c0 : c 0 ∈ bs
b : ℝ
hb : 1 + bs.max' ⋯ = b
n : ℕ
x : X
xs : x ∈ s
nN : N < n
H : dist (f N x) (f n x) < 1
cN : c N ∈ bs
bN : ‖f N x‖ ≤ bs.max' ⋯
⊢ ‖f n x‖ ≤ b
Tactic:
rw [dist_eq_norm] at H
Proof state after:
case neg
X Y : Type
inst✝¹ : TopologicalSpace X
inst✝ : NormedAddCommGroup Y
f : ℕ → X → Y
s : Set X
fc : ∀ (n : ℕ), ContinuousOn (f n) s
sc : IsCompact s
c : ℕ → ℝ
hc : (fun n => Classical.choose ⋯) = c
cs : ∀ (n : ℕ), 0 ≤ c n ∧ ∀ x ∈ s, ‖f n x‖ ≤ c n
N : ℕ
bs : Finset ℝ
hbs : Finset.image c (Finset.range (N + 1)) = bs
c0 : c 0 ∈ bs
b : ℝ
hb : 1 + bs.max' ⋯ = b
n : ℕ
x : X
xs : x ∈ s
nN : N < n
H : ‖f N x - f n x‖ < 1
cN : c N ∈ bs
bN : ‖f N x‖ ≤ bs.max' ⋯
⊢ ‖f n x‖ ≤ b
Theorem: UniformCauchySeqOn.bounded
Proof state before:
case neg
X Y : Type
inst✝¹ : TopologicalSpace X
inst✝ : NormedAddCommGroup Y
f : ℕ → X → Y
s : Set X
fc : ∀ (n : ℕ), ContinuousOn (f n) s
sc : IsCompact s
c : ℕ → ℝ
hc : (fun n => Classical.choose ⋯) = c
cs : ∀ (n : ℕ), 0 ≤ c n ∧ ∀ x ∈ s, ‖f n x‖ ≤ c n
N : ℕ
bs : Finset ℝ
hbs : Finset.image c (Finset.range (N + 1)) = bs
c0 : c 0 ∈ bs
b : ℝ
hb : 1 + bs.max' ⋯ = b
n : ℕ
x : X
xs : x ∈ s
nN : N < n
H : ‖f N x - f n x‖ < 1
cN : c N ∈ bs
bN : ‖f N x‖ ≤ bs.max' ⋯
⊢ ‖f n x‖ ≤ b
Tactic:
calc ‖f n x‖ = ‖f N x - (f N x - f n x)‖ := by rw [sub_sub_cancel]
  _ ≤ ‖f N x‖ + ‖f N x - f n x‖ := norm_sub_le _ _
  _ ≤ bs.max' _ + 1 := add_le_add bN H.le
  _ = 1 + bs.max' _ := by ring
  _ = b := by simp only [hb]
Proof state after:
no goals
Theorem: UniformCauchySeqOn.bounded
Proof state before:
X Y : Type
inst✝¹ : TopologicalSpace X
inst✝ : NormedAddCommGroup Y
f : ℕ → X → Y
s : Set X
fc : ∀ (n : ℕ), ContinuousOn (f n) s
sc : IsCompact s
c : ℕ → ℝ
hc : (fun n => Classical.choose ⋯) = c
cs : ∀ (n : ℕ), 0 ≤ c n ∧ ∀ x ∈ s, ‖f n x‖ ≤ c n
N : ℕ
bs : Finset ℝ
hbs : Finset.image c (Finset.range (N + 1)) = bs
c0 : c 0 ∈ bs
b : ℝ
hb : 1 + bs.max' ⋯ = b
n : ℕ
x : X
xs : x ∈ s
nN : N < n
H : dist (f N x) (f n x) < 1
⊢ c N ∈ bs
Tactic:
simp [← hbs]
Proof state after:
X Y : Type
inst✝¹ : TopologicalSpace X
inst✝ : NormedAddCommGroup Y
f : ℕ → X → Y
s : Set X
fc : ∀ (n : ℕ), ContinuousOn (f n) s
sc : IsCompact s
c : ℕ → ℝ
hc : (fun n => Classical.choose ⋯) = c
cs : ∀ (n : ℕ), 0 ≤ c n ∧ ∀ x ∈ s, ‖f n x‖ ≤ c n
N : ℕ
bs : Finset ℝ
hbs : Finset.image c (Finset.range (N + 1)) = bs
c0 : c 0 ∈ bs
b : ℝ
hb : 1 + bs.max' ⋯ = b
n : ℕ
x : X
xs : x ∈ s
nN : N < n
H : dist (f N x) (f n x) < 1
⊢ ∃ a < N + 1, c a = c N
Theorem: UniformCauchySeqOn.bounded
Proof state before:
X Y : Type
inst✝¹ : TopologicalSpace X
inst✝ : NormedAddCommGroup Y
f : ℕ → X → Y
s : Set X
fc : ∀ (n : ℕ), ContinuousOn (f n) s
sc : IsCompact s
c : ℕ → ℝ
hc : (fun n => Classical.choose ⋯) = c
cs : ∀ (n : ℕ), 0 ≤ c n ∧ ∀ x ∈ s, ‖f n x‖ ≤ c n
N : ℕ
bs : Finset ℝ
hbs : Finset.image c (Finset.range (N + 1)) = bs
c0 : c 0 ∈ bs
b : ℝ
hb : 1 + bs.max' ⋯ = b
n : ℕ
x : X
xs : x ∈ s
nN : N < n
H : dist (f N x) (f n x) < 1
⊢ ∃ a < N + 1, c a = c N
Tactic:
exists N
Proof state after:
X Y : Type
inst✝¹ : TopologicalSpace X
inst✝ : NormedAddCommGroup Y
f : ℕ → X → Y
s : Set X
fc : ∀ (n : ℕ), ContinuousOn (f n) s
sc : IsCompact s
c : ℕ → ℝ
hc : (fun n => Classical.choose ⋯) = c
cs : ∀ (n : ℕ), 0 ≤ c n ∧ ∀ x ∈ s, ‖f n x‖ ≤ c n
N : ℕ
bs : Finset ℝ
hbs : Finset.image c (Finset.range (N + 1)) = bs
c0 : c 0 ∈ bs
b : ℝ
hb : 1 + bs.max' ⋯ = b
n : ℕ
x : X
xs : x ∈ s
nN : N < n
H : dist (f N x) (f n x) < 1
⊢ N < N + 1 ∧ c N = c N
Theorem: UniformCauchySeqOn.bounded
Proof state before:
X Y : Type
inst✝¹ : TopologicalSpace X
inst✝ : NormedAddCommGroup Y
f : ℕ → X → Y
s : Set X
fc : ∀ (n : ℕ), ContinuousOn (f n) s
sc : IsCompact s
c : ℕ → ℝ
hc : (fun n => Classical.choose ⋯) = c
cs : ∀ (n : ℕ), 0 ≤ c n ∧ ∀ x ∈ s, ‖f n x‖ ≤ c n
N : ℕ
bs : Finset ℝ
hbs : Finset.image c (Finset.range (N + 1)) = bs
c0 : c 0 ∈ bs
b : ℝ
hb : 1 + bs.max' ⋯ = b
n : ℕ
x : X
xs : x ∈ s
nN : N < n
H : dist (f N x) (f n x) < 1
⊢ N < N + 1 ∧ c N = c N
Tactic:
simp
Proof state after:
no goals
Theorem: UniformCauchySeqOn.bounded
Proof state before:
X Y : Type
inst✝¹ : TopologicalSpace X
inst✝ : NormedAddCommGroup Y
f : ℕ → X → Y
s : Set X
fc : ∀ (n : ℕ), ContinuousOn (f n) s
sc : IsCompact s
c : ℕ → ℝ
hc : (fun n => Classical.choose ⋯) = c
cs : ∀ (n : ℕ), 0 ≤ c n ∧ ∀ x ∈ s, ‖f n x‖ ≤ c n
N : ℕ
bs : Finset ℝ
hbs : Finset.image c (Finset.range (N + 1)) = bs
c0 : c 0 ∈ bs
b : ℝ
hb : 1 + bs.max' ⋯ = b
n : ℕ
x : X
xs : x ∈ s
nN : N < n
H : ‖f N x - f n x‖ < 1
cN : c N ∈ bs
bN : ‖f N x‖ ≤ bs.max' ⋯
⊢ ‖f n x‖ = ‖f N x - (f N x - f n x)‖
Tactic:
rw [sub_sub_cancel]
Proof state after:
no goals
Theorem: UniformCauchySeqOn.bounded
Proof state before:
X Y : Type
inst✝¹ : TopologicalSpace X
inst✝ : NormedAddCommGroup Y
f : ℕ → X → Y
s : Set X
fc : ∀ (n : ℕ), ContinuousOn (f n) s
sc : IsCompact s
c : ℕ → ℝ
hc : (fun n => Classical.choose ⋯) = c
cs : ∀ (n : ℕ), 0 ≤ c n ∧ ∀ x ∈ s, ‖f n x‖ ≤ c n
N : ℕ
bs : Finset ℝ
hbs : Finset.image c (Finset.range (N + 1)) = bs
c0 : c 0 ∈ bs
b : ℝ
hb : 1 + bs.max' ⋯ = b
n : ℕ
x : X
xs : x ∈ s
nN : N < n
H : ‖f N x - f n x‖ < 1
cN : c N ∈ bs
bN : ‖f N x‖ ≤ bs.max' ⋯
⊢ bs.max' ⋯ + 1 = 1 + bs.max' ?m.16989
Tactic:
ring
Proof state after:
no goals
Theorem: UniformCauchySeqOn.bounded
Proof state before:
X Y : Type
inst✝¹ : TopologicalSpace X
inst✝ : NormedAddCommGroup Y
f : ℕ → X → Y
s : Set X
fc : ∀ (n : ℕ), ContinuousOn (f n) s
sc : IsCompact s
c : ℕ → ℝ
hc : (fun n => Classical.choose ⋯) = c
cs : ∀ (n : ℕ), 0 ≤ c n ∧ ∀ x ∈ s, ‖f n x‖ ≤ c n
N : ℕ
bs : Finset ℝ
hbs : Finset.image c (Finset.range (N + 1)) = bs
c0 : c 0 ∈ bs
b : ℝ
hb : 1 + bs.max' ⋯ = b
n : ℕ
x : X
xs : x ∈ s
nN : N < n
H : ‖f N x - f n x‖ < 1
cN : c N ∈ bs
bN : ‖f N x‖ ≤ bs.max' ⋯
⊢ 1 + bs.max' ⋯ = b
Tactic:
simp only [hb]
Proof state after:
no goals
Theorem: tendsto_inv_iff_tendsto
Proof state before:
A B : Type
inst✝ : NontriviallyNormedField B
l : Filter A
f : A → B
a : B
a0 : a ≠ 0
⊢ Tendsto (fun x => (f x)⁻¹) l (𝓝 a⁻¹) ↔ Tendsto f l (𝓝 a)
Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ h.inv₀ a0⟩
Proof state after:
A B : Type
inst✝ : NontriviallyNormedField B
l : Filter A
f : A → B
a : B
a0 : a ≠ 0
h : Tendsto (fun x => (f x)⁻¹) l (𝓝 a⁻¹)
⊢ Tendsto f l (𝓝 a)
Theorem: tendsto_inv_iff_tendsto
Proof state before:
A B : Type
inst✝ : NontriviallyNormedField B
l : Filter A
f : A → B
a : B
a0 : a ≠ 0
h : Tendsto (fun x => (f x)⁻¹) l (𝓝 a⁻¹)
⊢ Tendsto f l (𝓝 a)
Tactic:
have h := h.inv₀ (inv_ne_zero a0)
Proof state after:
A B : Type
inst✝ : NontriviallyNormedField B
l : Filter A
f : A → B
a : B
a0 : a ≠ 0
h✝ : Tendsto (fun x => (f x)⁻¹) l (𝓝 a⁻¹)
h : Tendsto (fun x => (f x)⁻¹⁻¹) l (𝓝 a⁻¹⁻¹)
⊢ Tendsto f l (𝓝 a)
Theorem: tendsto_inv_iff_tendsto
Proof state before:
A B : Type
inst✝ : NontriviallyNormedField B
l : Filter A
f : A → B
a : B
a0 : a ≠ 0
h✝ : Tendsto (fun x => (f x)⁻¹) l (𝓝 a⁻¹)
h : Tendsto (fun x => (f x)⁻¹⁻¹) l (𝓝 a⁻¹⁻¹)
⊢ Tendsto f l (𝓝 a)
Tactic:
field_simp [a0] at h
Proof state after:
A B : Type
inst✝ : NontriviallyNormedField B
l : Filter A
f : A → B
a : B
a0 : a ≠ 0
h✝ : Tendsto (fun x => (f x)⁻¹) l (𝓝 a⁻¹)
h : Tendsto (fun x => f x) l (𝓝 a)
⊢ Tendsto f l (𝓝 a)
Theorem: tendsto_inv_iff_tendsto
Proof state before:
A B : Type
inst✝ : NontriviallyNormedField B
l : Filter A
f : A → B
a : B
a0 : a ≠ 0
h✝ : Tendsto (fun x => (f x)⁻¹) l (𝓝 a⁻¹)
h : Tendsto (fun x => f x) l (𝓝 a)
⊢ Tendsto f l (𝓝 a)
Tactic:
exact h
Proof state after:
no goals
Theorem: IsClosed.Icc_subset_of_forall_mem_nhds_within'
Proof state before:
X : Type
inst✝³ : ConditionallyCompleteLinearOrder X
inst✝² : TopologicalSpace X
inst✝¹ : OrderTopology X
inst✝ : DenselyOrdered X
a b : X
s : Set X
sc : IsClosed (s ∩ Icc a b)
sb : b ∈ s
so : ∀ x ∈ s ∩ Ioc a b, s ∈ 𝓝[<] x
⊢ Icc a b ⊆ s
Tactic:
generalize hs' : ofDual ⁻¹' s = s'
Proof state after:
X : Type
inst✝³ : ConditionallyCompleteLinearOrder X
inst✝² : TopologicalSpace X
inst✝¹ : OrderTopology X
inst✝ : DenselyOrdered X
a b : X
s : Set X
sc : IsClosed (s ∩ Icc a b)
sb : b ∈ s
so : ∀ x ∈ s ∩ Ioc a b, s ∈ 𝓝[<] x
s' : Set Xᵒᵈ
hs' : ⇑ofDual ⁻¹' s = s'
⊢ Icc a b ⊆ s
Theorem: IsClosed.Icc_subset_of_forall_mem_nhds_within'
Proof state before:
X : Type
inst✝³ : ConditionallyCompleteLinearOrder X
inst✝² : TopologicalSpace X
inst✝¹ : OrderTopology X
inst✝ : DenselyOrdered X
a b : X
s : Set X
sc : IsClosed (s ∩ Icc a b)
sb : b ∈ s
so : ∀ x ∈ s ∩ Ioc a b, s ∈ 𝓝[<] x
s' : Set Xᵒᵈ
hs' : ⇑ofDual ⁻¹' s = s'
rev : Icc (toDual b) (toDual a) ⊆ s'
⊢ Icc a b ⊆ s
Tactic:
intro x m
Proof state after:
X : Type
inst✝³ : ConditionallyCompleteLinearOrder X
inst✝² : TopologicalSpace X
inst✝¹ : OrderTopology X
inst✝ : DenselyOrdered X
a b : X
s : Set X
sc : IsClosed (s ∩ Icc a b)
sb : b ∈ s
so : ∀ x ∈ s ∩ Ioc a b, s ∈ 𝓝[<] x
s' : Set Xᵒᵈ
hs' : ⇑ofDual ⁻¹' s = s'
rev : Icc (toDual b) (toDual a) ⊆ s'
x : X
m : x ∈ Icc a b
⊢ x ∈ s
Theorem: IsClosed.Icc_subset_of_forall_mem_nhds_within'
Proof state before:
X : Type
inst✝³ : ConditionallyCompleteLinearOrder X
inst✝² : TopologicalSpace X
inst✝¹ : OrderTopology X
inst✝ : DenselyOrdered X
a b : X
s : Set X
sc : IsClosed (s ∩ Icc a b)
sb : b ∈ s
so : ∀ x ∈ s ∩ Ioc a b, s ∈ 𝓝[<] x
s' : Set Xᵒᵈ
hs' : ⇑ofDual ⁻¹' s = s'
rev : Icc (toDual b) (toDual a) ⊆ s'
x : X
m : x ∈ Icc a b
⊢ x ∈ s
Tactic:
simp only [Set.mem_Icc] at m
Proof state after:
X : Type
inst✝³ : ConditionallyCompleteLinearOrder X
inst✝² : TopologicalSpace X
inst✝¹ : OrderTopology X
inst✝ : DenselyOrdered X
a b : X
s : Set X
sc : IsClosed (s ∩ Icc a b)
sb : b ∈ s
so : ∀ x ∈ s ∩ Ioc a b, s ∈ 𝓝[<] x
s' : Set Xᵒᵈ
hs' : ⇑ofDual ⁻¹' s = s'
rev : Icc (toDual b) (toDual a) ⊆ s'
x : X
m : a ≤ x ∧ x ≤ b
⊢ x ∈ s
Theorem: IsClosed.Icc_subset_of_forall_mem_nhds_within'
Proof state before:
X : Type
inst✝³ : ConditionallyCompleteLinearOrder X
inst✝² : TopologicalSpace X
inst✝¹ : OrderTopology X
inst✝ : DenselyOrdered X
a b : X
s : Set X
sc : IsClosed (s ∩ Icc a b)
sb : b ∈ s
so : ∀ x ∈ s ∩ Ioc a b, s ∈ 𝓝[<] x
s' : Set Xᵒᵈ
hs' : ⇑ofDual ⁻¹' s = s'
rev : Icc (toDual b) (toDual a) ⊆ s'
x : X
m : a ≤ x ∧ x ≤ b
⊢ x ∈ s
Tactic:
specialize @rev (toDual x)
Proof state after:
X : Type
inst✝³ : ConditionallyCompleteLinearOrder X
inst✝² : TopologicalSpace X
inst✝¹ : OrderTopology X
inst✝ : DenselyOrdered X
a b : X
s : Set X
sc : IsClosed (s ∩ Icc a b)
sb : b ∈ s
so : ∀ x ∈ s ∩ Ioc a b, s ∈ 𝓝[<] x
s' : Set Xᵒᵈ
hs' : ⇑ofDual ⁻¹' s = s'
x : X
m : a ≤ x ∧ x ≤ b
rev : toDual x ∈ Icc (toDual b) (toDual a) → toDual x ∈ s'
⊢ x ∈ s
Theorem: IsClosed.Icc_subset_of_forall_mem_nhds_within'
Proof state before:
X : Type
inst✝³ : ConditionallyCompleteLinearOrder X
inst✝² : TopologicalSpace X
inst✝¹ : OrderTopology X
inst✝ : DenselyOrdered X
a b : X
s : Set X
sc : IsClosed (s ∩ Icc a b)
sb : b ∈ s
so : ∀ x ∈ s ∩ Ioc a b, s ∈ 𝓝[<] x
s' : Set Xᵒᵈ
hs' : ⇑ofDual ⁻¹' s = s'
x : X
m : a ≤ x ∧ x ≤ b
rev : toDual x ∈ Icc (toDual b) (toDual a) → toDual x ∈ s'
⊢ x ∈ s
Tactic:
simp only [Set.dual_Icc, Set.mem_preimage, Set.mem_Icc, and_imp, OrderDual.ofDual_toDual,
  ← hs'] at rev
Proof state after:
X : Type
inst✝³ : ConditionallyCompleteLinearOrder X
inst✝² : TopologicalSpace X
inst✝¹ : OrderTopology X
inst✝ : DenselyOrdered X
a b : X
s : Set X
sc : IsClosed (s ∩ Icc a b)
sb : b ∈ s
so : ∀ x ∈ s ∩ Ioc a b, s ∈ 𝓝[<] x
s' : Set Xᵒᵈ
hs' : ⇑ofDual ⁻¹' s = s'
x : X
m : a ≤ x ∧ x ≤ b
rev : a ≤ x → x ≤ b → x ∈ s
⊢ x ∈ s
Theorem: IsClosed.Icc_subset_of_forall_mem_nhds_within'
Proof state before:
X : Type
inst✝³ : ConditionallyCompleteLinearOrder X
inst✝² : TopologicalSpace X
inst✝¹ : OrderTopology X
inst✝ : DenselyOrdered X
a b : X
s : Set X
sc : IsClosed (s ∩ Icc a b)
sb : b ∈ s
so : ∀ x ∈ s ∩ Ioc a b, s ∈ 𝓝[<] x
s' : Set Xᵒᵈ
hs' : ⇑ofDual ⁻¹' s = s'
x : X
m : a ≤ x ∧ x ≤ b
rev : a ≤ x → x ≤ b → x ∈ s
⊢ x ∈ s
Tactic:
exact rev m.1 m.2
Proof state after:
no goals
Theorem: IsClosed.Icc_subset_of_forall_mem_nhds_within'
Proof state before:
X : Type
inst✝³ : ConditionallyCompleteLinearOrder X
inst✝² : TopologicalSpace X
inst✝¹ : OrderTopology X
inst✝ : DenselyOrdered X
a b : X
s : Set X
sc : IsClosed (s ∩ Icc a b)
sb : b ∈ s
so : ∀ x ∈ s ∩ Ioc a b, s ∈ 𝓝[<] x
s' : Set Xᵒᵈ
hs' : ⇑ofDual ⁻¹' s = s'
⊢ Icc (toDual b) (toDual a) ⊆ s'
Tactic:
apply IsClosed.Icc_subset_of_forall_mem_nhdsWithin
Proof state after:
case hs
X : Type
inst✝³ : ConditionallyCompleteLinearOrder X
inst✝² : TopologicalSpace X
inst✝¹ : OrderTopology X
inst✝ : DenselyOrdered X
a b : X
s : Set X
sc : IsClosed (s ∩ Icc a b)
sb : b ∈ s
so : ∀ x ∈ s ∩ Ioc a b, s ∈ 𝓝[<] x
s' : Set Xᵒᵈ
hs' : ⇑ofDual ⁻¹' s = s'
⊢ IsClosed (s' ∩ Icc (toDual b) (toDual a))

case ha
X : Type
inst✝³ : ConditionallyCompleteLinearOrder X
inst✝² : TopologicalSpace X
inst✝¹ : OrderTopology X
inst✝ : DenselyOrdered X
a b : X
s : Set X
sc : IsClosed (s ∩ Icc a b)
sb : b ∈ s
so : ∀ x ∈ s ∩ Ioc a b, s ∈ 𝓝[<] x
s' : Set Xᵒᵈ
hs' : ⇑ofDual ⁻¹' s = s'
⊢ toDual b ∈ s'

case hgt
X : Type
inst✝³ : ConditionallyCompleteLinearOrder X
inst✝² : TopologicalSpace X
inst✝¹ : OrderTopology X
inst✝ : DenselyOrdered X
a b : X
s : Set X
sc : IsClosed (s ∩ Icc a b)
sb : b ∈ s
so : ∀ x ∈ s ∩ Ioc a b, s ∈ 𝓝[<] x
s' : Set Xᵒᵈ
hs' : ⇑ofDual ⁻¹' s = s'
⊢ ∀ x ∈ s' ∩ Ico (toDual b) (toDual a), s' ∈ 𝓝[>] x
Theorem: IsClosed.Icc_subset_of_forall_mem_nhds_within'
Proof state before:
case hs
X : Type
inst✝³ : ConditionallyCompleteLinearOrder X
inst✝² : TopologicalSpace X
inst✝¹ : OrderTopology X
inst✝ : DenselyOrdered X
a b : X
s : Set X
sc : IsClosed (s ∩ Icc a b)
sb : b ∈ s
so : ∀ x ∈ s ∩ Ioc a b, s ∈ 𝓝[<] x
s' : Set Xᵒᵈ
hs' : ⇑ofDual ⁻¹' s = s'
⊢ IsClosed (s' ∩ Icc (toDual b) (toDual a))
Tactic:
have e : s' ∩ Icc (toDual b) (toDual a) = ofDual ⁻¹' (s ∩ Icc a b) := by
  apply Set.ext; intro x; simp only [Set.dual_Icc, Set.preimage_inter, ← hs']
Proof state after:
case hs
X : Type
inst✝³ : ConditionallyCompleteLinearOrder X
inst✝² : TopologicalSpace X
inst✝¹ : OrderTopology X
inst✝ : DenselyOrdered X
a b : X
s : Set X
sc : IsClosed (s ∩ Icc a b)
sb : b ∈ s
so : ∀ x ∈ s ∩ Ioc a b, s ∈ 𝓝[<] x
s' : Set Xᵒᵈ
hs' : ⇑ofDual ⁻¹' s = s'
e : s' ∩ Icc (toDual b) (toDual a) = ⇑ofDual ⁻¹' (s ∩ Icc a b)
⊢ IsClosed (s' ∩ Icc (toDual b) (toDual a))
Theorem: IsClosed.Icc_subset_of_forall_mem_nhds_within'
Proof state before:
case hs
X : Type
inst✝³ : ConditionallyCompleteLinearOrder X
inst✝² : TopologicalSpace X
inst✝¹ : OrderTopology X
inst✝ : DenselyOrdered X
a b : X
s : Set X
sc : IsClosed (s ∩ Icc a b)
sb : b ∈ s
so : ∀ x ∈ s ∩ Ioc a b, s ∈ 𝓝[<] x
s' : Set Xᵒᵈ
hs' : ⇑ofDual ⁻¹' s = s'
e : s' ∩ Icc (toDual b) (toDual a) = ⇑ofDual ⁻¹' (s ∩ Icc a b)
⊢ IsClosed (s' ∩ Icc (toDual b) (toDual a))
Tactic:
rw [e]
Proof state after:
case hs
X : Type
inst✝³ : ConditionallyCompleteLinearOrder X
inst✝² : TopologicalSpace X
inst✝¹ : OrderTopology X
inst✝ : DenselyOrdered X
a b : X
s : Set X
sc : IsClosed (s ∩ Icc a b)
sb : b ∈ s
so : ∀ x ∈ s ∩ Ioc a b, s ∈ 𝓝[<] x
s' : Set Xᵒᵈ
hs' : ⇑ofDual ⁻¹' s = s'
e : s' ∩ Icc (toDual b) (toDual a) = ⇑ofDual ⁻¹' (s ∩ Icc a b)
⊢ IsClosed (⇑ofDual ⁻¹' (s ∩ Icc a b))
Theorem: IsClosed.Icc_subset_of_forall_mem_nhds_within'
Proof state before:
case hs
X : Type
inst✝³ : ConditionallyCompleteLinearOrder X
inst✝² : TopologicalSpace X
inst✝¹ : OrderTopology X
inst✝ : DenselyOrdered X
a b : X
s : Set X
sc : IsClosed (s ∩ Icc a b)
sb : b ∈ s
so : ∀ x ∈ s ∩ Ioc a b, s ∈ 𝓝[<] x
s' : Set Xᵒᵈ
hs' : ⇑ofDual ⁻¹' s = s'
e : s' ∩ Icc (toDual b) (toDual a) = ⇑ofDual ⁻¹' (s ∩ Icc a b)
⊢ IsClosed (⇑ofDual ⁻¹' (s ∩ Icc a b))
Tactic:
exact IsClosed.preimage continuous_ofDual sc
Proof state after:
no goals
Theorem: IsClosed.Icc_subset_of_forall_mem_nhds_within'
Proof state before:
X : Type
inst✝³ : ConditionallyCompleteLinearOrder X
inst✝² : TopologicalSpace X
inst✝¹ : OrderTopology X
inst✝ : DenselyOrdered X
a b : X
s : Set X
sc : IsClosed (s ∩ Icc a b)
sb : b ∈ s
so : ∀ x ∈ s ∩ Ioc a b, s ∈ 𝓝[<] x
s' : Set Xᵒᵈ
hs' : ⇑ofDual ⁻¹' s = s'
⊢ s' ∩ Icc (toDual b) (toDual a) = ⇑ofDual ⁻¹' (s ∩ Icc a b)
Tactic:
apply Set.ext
Proof state after:
case h
X : Type
inst✝³ : ConditionallyCompleteLinearOrder X
inst✝² : TopologicalSpace X
inst✝¹ : OrderTopology X
inst✝ : DenselyOrdered X
a b : X
s : Set X
sc : IsClosed (s ∩ Icc a b)
sb : b ∈ s
so : ∀ x ∈ s ∩ Ioc a b, s ∈ 𝓝[<] x
s' : Set Xᵒᵈ
hs' : ⇑ofDual ⁻¹' s = s'
⊢ ∀ (x : Xᵒᵈ), x ∈ s' ∩ Icc (toDual b) (toDual a) ↔ x ∈ ⇑ofDual ⁻¹' (s ∩ Icc a b)
Theorem: IsClosed.Icc_subset_of_forall_mem_nhds_within'
Proof state before:
case h
X : Type
inst✝³ : ConditionallyCompleteLinearOrder X
inst✝² : TopologicalSpace X
inst✝¹ : OrderTopology X
inst✝ : DenselyOrdered X
a b : X
s : Set X
sc : IsClosed (s ∩ Icc a b)
sb : b ∈ s
so : ∀ x ∈ s ∩ Ioc a b, s ∈ 𝓝[<] x
s' : Set Xᵒᵈ
hs' : ⇑ofDual ⁻¹' s = s'
⊢ ∀ (x : Xᵒᵈ), x ∈ s' ∩ Icc (toDual b) (toDual a) ↔ x ∈ ⇑ofDual ⁻¹' (s ∩ Icc a b)
Tactic:
intro x
Proof state after:
case h
X : Type
inst✝³ : ConditionallyCompleteLinearOrder X
inst✝² : TopologicalSpace X
inst✝¹ : OrderTopology X
inst✝ : DenselyOrdered X
a b : X
s : Set X
sc : IsClosed (s ∩ Icc a b)
sb : b ∈ s
so : ∀ x ∈ s ∩ Ioc a b, s ∈ 𝓝[<] x
s' : Set Xᵒᵈ
hs' : ⇑ofDual ⁻¹' s = s'
x : Xᵒᵈ
⊢ x ∈ s' ∩ Icc (toDual b) (toDual a) ↔ x ∈ ⇑ofDual ⁻¹' (s ∩ Icc a b)
Theorem: IsClosed.Icc_subset_of_forall_mem_nhds_within'
Proof state before:
case h
X : Type
inst✝³ : ConditionallyCompleteLinearOrder X
inst✝² : TopologicalSpace X
inst✝¹ : OrderTopology X
inst✝ : DenselyOrdered X
a b : X
s : Set X
sc : IsClosed (s ∩ Icc a b)
sb : b ∈ s
so : ∀ x ∈ s ∩ Ioc a b, s ∈ 𝓝[<] x
s' : Set Xᵒᵈ
hs' : ⇑ofDual ⁻¹' s = s'
x : Xᵒᵈ
⊢ x ∈ s' ∩ Icc (toDual b) (toDual a) ↔ x ∈ ⇑ofDual ⁻¹' (s ∩ Icc a b)
Tactic:
simp only [Set.dual_Icc, Set.preimage_inter, ← hs']
Proof state after:
no goals
Theorem: IsClosed.Icc_subset_of_forall_mem_nhds_within'
Proof state before:
case ha
X : Type
inst✝³ : ConditionallyCompleteLinearOrder X
inst✝² : TopologicalSpace X
inst✝¹ : OrderTopology X
inst✝ : DenselyOrdered X
a b : X
s : Set X
sc : IsClosed (s ∩ Icc a b)
sb : b ∈ s
so : ∀ x ∈ s ∩ Ioc a b, s ∈ 𝓝[<] x
s' : Set Xᵒᵈ
hs' : ⇑ofDual ⁻¹' s = s'
⊢ toDual b ∈ s'
Tactic:
simp only [Set.mem_preimage, OrderDual.ofDual_toDual, sb, ← hs']
Proof state after:
no goals
Theorem: IsClosed.Icc_subset_of_forall_mem_nhds_within'
Proof state before:
case hgt
X : Type
inst✝³ : ConditionallyCompleteLinearOrder X
inst✝² : TopologicalSpace X
inst✝¹ : OrderTopology X
inst✝ : DenselyOrdered X
a b : X
s : Set X
sc : IsClosed (s ∩ Icc a b)
sb : b ∈ s
so : ∀ x ∈ s ∩ Ioc a b, s ∈ 𝓝[<] x
s' : Set Xᵒᵈ
hs' : ⇑ofDual ⁻¹' s = s'
⊢ ∀ x ∈ s' ∩ Ico (toDual b) (toDual a), s' ∈ 𝓝[>] x
Tactic:
intro x m
Proof state after:
case hgt
X : Type
inst✝³ : ConditionallyCompleteLinearOrder X
inst✝² : TopologicalSpace X
inst✝¹ : OrderTopology X
inst✝ : DenselyOrdered X
a b : X
s : Set X
sc : IsClosed (s ∩ Icc a b)
sb : b ∈ s
so : ∀ x ∈ s ∩ Ioc a b, s ∈ 𝓝[<] x
s' : Set Xᵒᵈ
hs' : ⇑ofDual ⁻¹' s = s'
x : Xᵒᵈ
m : x ∈ s' ∩ Ico (toDual b) (toDual a)
⊢ s' ∈ 𝓝[>] x
Theorem: IsClosed.Icc_subset_of_forall_mem_nhds_within'
Proof state before:
case hgt
X : Type
inst✝³ : ConditionallyCompleteLinearOrder X
inst✝² : TopologicalSpace X
inst✝¹ : OrderTopology X
inst✝ : DenselyOrdered X
a b : X
s : Set X
sc : IsClosed (s ∩ Icc a b)
sb : b ∈ s
so : ∀ x ∈ s ∩ Ioc a b, s ∈ 𝓝[<] x
s' : Set Xᵒᵈ
hs' : ⇑ofDual ⁻¹' s = s'
x : Xᵒᵈ
m : x ∈ s' ∩ Ico (toDual b) (toDual a)
⊢ s' ∈ 𝓝[>] x
Tactic:
simp only [Set.mem_preimage, Set.mem_inter_iff, Set.mem_Ico, OrderDual.toDual_le,
  OrderDual.lt_toDual] at m
Proof state after:
case hgt
X : Type
inst✝³ : ConditionallyCompleteLinearOrder X
inst✝² : TopologicalSpace X
inst✝¹ : OrderTopology X
inst✝ : DenselyOrdered X
a b : X
s : Set X
sc : IsClosed (s ∩ Icc a b)
sb : b ∈ s
so : ∀ x ∈ s ∩ Ioc a b, s ∈ 𝓝[<] x
s' : Set Xᵒᵈ
hs' : ⇑ofDual ⁻¹' s = s'
x : Xᵒᵈ
m : x ∈ s' ∧ ofDual x ≤ b ∧ a < ofDual x
⊢ s' ∈ 𝓝[>] x
Theorem: IsClosed.Icc_subset_of_forall_mem_nhds_within'
Proof state before:
case hgt
X : Type
inst✝³ : ConditionallyCompleteLinearOrder X
inst✝² : TopologicalSpace X
inst✝¹ : OrderTopology X
inst✝ : DenselyOrdered X
a b : X
s : Set X
sc : IsClosed (s ∩ Icc a b)
sb : b ∈ s
so : ∀ x ∈ s ∩ Ioc a b, s ∈ 𝓝[<] x
s' : Set Xᵒᵈ
hs' : ⇑ofDual ⁻¹' s = s'
x : Xᵒᵈ
m : x ∈ s' ∧ ofDual x ≤ b ∧ a < ofDual x
⊢ s' ∈ 𝓝[>] x
Tactic:
simp only [mem_nhdsWithin_iff_eventually, eventually_nhds_iff, Set.mem_inter_iff,
  Set.mem_Ioc, ← hs'] at so m ⊢
Proof state after:
case hgt
X : Type
inst✝³ : ConditionallyCompleteLinearOrder X
inst✝² : TopologicalSpace X
inst✝¹ : OrderTopology X
inst✝ : DenselyOrdered X
a b : X
s : Set X
sc : IsClosed (s ∩ Icc a b)
sb : b ∈ s
s' : Set Xᵒᵈ
hs' : ⇑ofDual ⁻¹' s = s'
x : Xᵒᵈ
so : ∀ (x : X), x ∈ s ∧ a < x ∧ x ≤ b → ∃ t, (∀ x_1 ∈ t, x_1 ∈ Iio x → x_1 ∈ s) ∧ IsOpen t ∧ x ∈ t
m : x ∈ ⇑ofDual ⁻¹' s ∧ ofDual x ≤ b ∧ a < ofDual x
⊢ ∃ t, (∀ x_1 ∈ t, x_1 ∈ Ioi x → x_1 ∈ ⇑ofDual ⁻¹' s) ∧ IsOpen t ∧ x ∈ t