α : Type u
β : Type v
ι✝ : Type ?u.62603
R : Type u_2
inst✝³ : CompleteLinearOrder R
inst✝² : TopologicalSpace R
inst✝¹ : OrderTopology R
ι : Type u_1
x : R
as : ι → R
x_lt : ∀ (i : ι), x < as i
F : Filter ι
inst✝ : NeBot F
as_lim : Tendsto as F (𝓝 x)
obs : ¬x ∈ range as
⊢ (⋃ (i : ι), Ici (as i)) = Ioi x
α : Type u
β : Type v
ι✝ : Type ?u.62603
R : Type u_2
inst✝³ : CompleteLinearOrder R
inst✝² : TopologicalSpace R
inst✝¹ : OrderTopology R
ι : Type u_1
x : R
as : ι → R
x_lt : ∀ (i : ι), x < as i
F : Filter ι
inst✝ : NeBot F
as_lim : Tendsto as F (𝓝 x)
⊢ (⋃ (i : ι), Ici (as i)) = Ioi x
have obs : x ∉ range as := by
  intro maybe_x_is
  rcases mem_range.mp maybe_x_is with ⟨i, hi⟩
  simpa only [hi, lt_self_iff_false] using x_lt i
α : Type u
β : Type v
ι✝ : Type ?u.62603
R : Type u_2
inst✝³ : CompleteLinearOrder R
inst✝² : TopologicalSpace R
inst✝¹ : OrderTopology R
ι : Type u_1
x : R
as : ι → R
x_lt : ∀ (i : ι), x < as i
F : Filter ι
inst✝ : NeBot F
as_lim : Tendsto as F (𝓝 x)
obs : ¬x ∈ range as
this : (⨅ (i : ι), as i) = x
⊢ (⋃ (i : ι), Ici (as i)) = Ioi x
α : Type u
β : Type v
ι✝ : Type ?u.62603
R : Type u_2
inst✝³ : CompleteLinearOrder R
inst✝² : TopologicalSpace R
inst✝¹ : OrderTopology R
ι : Type u_1
x : R
as : ι → R
x_lt : ∀ (i : ι), x < as i
F : Filter ι
inst✝ : NeBot F
as_lim : Tendsto as F (𝓝 x)
obs : ¬x ∈ range as
⊢ (⋃ (i : ι), Ici (as i)) = Ioi x
have := iInf_eq_of_forall_le_of_tendsto (fun i ↦ (x_lt i).le) as_lim
α : Type u
β : Type v
ι✝ : Type ?u.62603
R : Type u_2
inst✝³ : CompleteLinearOrder R
inst✝² : TopologicalSpace R
inst✝¹ : OrderTopology R
ι : Type u_1
x : R
as : ι → R
x_lt : ∀ (i : ι), x < as i
F : Filter ι
inst✝ : NeBot F
as_lim : Tendsto as F (𝓝 x)
obs : ¬(⨅ (i : ι), as i) ∈ range as
this : (⨅ (i : ι), as i) = x
⊢ (⋃ (i : ι), Ici (as i)) = Ioi x
α : Type u
β : Type v
ι✝ : Type ?u.62603
R : Type u_2
inst✝³ : CompleteLinearOrder R
inst✝² : TopologicalSpace R
inst✝¹ : OrderTopology R
ι : Type u_1
x : R
as : ι → R
x_lt : ∀ (i : ι), x < as i
F : Filter ι
inst✝ : NeBot F
as_lim : Tendsto as F (𝓝 x)
obs : ¬x ∈ range as
this : (⨅ (i : ι), as i) = x
⊢ (⋃ (i : ι), Ici (as i)) = Ioi x
rw [← this] at obs
α : Type u
β : Type v
ι✝ : Type ?u.62603
R : Type u_2
inst✝³ : CompleteLinearOrder R
inst✝² : TopologicalSpace R
inst✝¹ : OrderTopology R
ι : Type u_1
x : R
as : ι → R
x_lt : ∀ (i : ι), x < as i
F : Filter ι
inst✝ : NeBot F
as_lim : Tendsto as F (𝓝 x)
obs : ¬(⨅ (i : ι), as i) ∈ range as
this : (⨅ (i : ι), as i) = x
⊢ (⋃ (i : ι), Ici (as i)) = Ioi (⨅ (i : ι), as i)
α : Type u
β : Type v
ι✝ : Type ?u.62603
R : Type u_2
inst✝³ : CompleteLinearOrder R
inst✝² : TopologicalSpace R
inst✝¹ : OrderTopology R
ι : Type u_1
x : R
as : ι → R
x_lt : ∀ (i : ι), x < as i
F : Filter ι
inst✝ : NeBot F
as_lim : Tendsto as F (𝓝 x)
obs : ¬(⨅ (i : ι), as i) ∈ range as
this : (⨅ (i : ι), as i) = x
⊢ (⋃ (i : ι), Ici (as i)) = Ioi x
rw [← this]
no goals
α : Type u
β : Type v
ι✝ : Type ?u.62603
R : Type u_2
inst✝³ : CompleteLinearOrder R
inst✝² : TopologicalSpace R
inst✝¹ : OrderTopology R
ι : Type u_1
x : R
as : ι → R
x_lt : ∀ (i : ι), x < as i
F : Filter ι
inst✝ : NeBot F
as_lim : Tendsto as F (𝓝 x)
obs : ¬(⨅ (i : ι), as i) ∈ range as
this : (⨅ (i : ι), as i) = x
⊢ (⋃ (i : ι), Ici (as i)) = Ioi (⨅ (i : ι), as i)
exact iUnion_Ici_eq_Ioi_iInf obs
α : Type u
β : Type v
ι✝ : Type ?u.62603
R : Type u_2
inst✝³ : CompleteLinearOrder R
inst✝² : TopologicalSpace R
inst✝¹ : OrderTopology R
ι : Type u_1
x : R
as : ι → R
x_lt : ∀ (i : ι), x < as i
F : Filter ι
inst✝ : NeBot F
as_lim : Tendsto as F (𝓝 x)
maybe_x_is : x ∈ range as
⊢ False
α : Type u
β : Type v
ι✝ : Type ?u.62603
R : Type u_2
inst✝³ : CompleteLinearOrder R
inst✝² : TopologicalSpace R
inst✝¹ : OrderTopology R
ι : Type u_1
x : R
as : ι → R
x_lt : ∀ (i : ι), x < as i
F : Filter ι
inst✝ : NeBot F
as_lim : Tendsto as F (𝓝 x)
⊢ ¬x ∈ range as
intro maybe_x_is
case intro
α : Type u
β : Type v
ι✝ : Type ?u.62603
R : Type u_2
inst✝³ : CompleteLinearOrder R
inst✝² : TopologicalSpace R
inst✝¹ : OrderTopology R
ι : Type u_1
x : R
as : ι → R
x_lt : ∀ (i : ι), x < as i
F : Filter ι
inst✝ : NeBot F
as_lim : Tendsto as F (𝓝 x)
maybe_x_is : x ∈ range as
i : ι
hi : as i = x
⊢ False
α : Type u
β : Type v
ι✝ : Type ?u.62603
R : Type u_2
inst✝³ : CompleteLinearOrder R
inst✝² : TopologicalSpace R
inst✝¹ : OrderTopology R
ι : Type u_1
x : R
as : ι → R
x_lt : ∀ (i : ι), x < as i
F : Filter ι
inst✝ : NeBot F
as_lim : Tendsto as F (𝓝 x)
maybe_x_is : x ∈ range as
⊢ False
rcases mem_range.mp maybe_x_is with ⟨i, hi⟩
no goals
case intro
α : Type u
β : Type v
ι✝ : Type ?u.62603
R : Type u_2
inst✝³ : CompleteLinearOrder R
inst✝² : TopologicalSpace R
inst✝¹ : OrderTopology R
ι : Type u_1
x : R
as : ι → R
x_lt : ∀ (i : ι), x < as i
F : Filter ι
inst✝ : NeBot F
as_lim : Tendsto as F (𝓝 x)
maybe_x_is : x ∈ range as
i : ι
hi : as i = x
⊢ False
simpa only [hi, lt_self_iff_false] using x_lt i