case inl
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
hs : s ∈ 𝓝[Ici a] a
ha : IsMax a
⊢ ∃ b, a ≤ b ∧ Icc a b ∈ 𝓝[Ici a] a ∧ Icc a b ⊆ s

case inr
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
hs : s ∈ 𝓝[Ici a] a
ha : ∃ b, a < b
⊢ ∃ b, a ≤ b ∧ Icc a b ∈ 𝓝[Ici a] a ∧ Icc a b ⊆ s
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
hs : s ∈ 𝓝[Ici a] a
⊢ ∃ b, a ≤ b ∧ Icc a b ∈ 𝓝[Ici a] a ∧ Icc a b ⊆ s
rcases (em (IsMax a)).imp_right not_isMax_iff.mp with (ha | ha)
case inl
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
hs : s ∈ 𝓝[Ici a] a
ha : IsMax a
⊢ a ≤ a ∧ Icc a a ∈ 𝓝[Ici a] a ∧ Icc a a ⊆ s
case inl
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
hs : s ∈ 𝓝[Ici a] a
ha : IsMax a
⊢ ∃ b, a ≤ b ∧ Icc a b ∈ 𝓝[Ici a] a ∧ Icc a b ⊆ s
use a
no goals
case inl
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
hs : s ∈ 𝓝[Ici a] a
ha : IsMax a
⊢ a ≤ a ∧ Icc a a ∈ 𝓝[Ici a] a ∧ Icc a a ⊆ s
simpa [ha.Ici_eq] using hs
case inr.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
hs : s ∈ 𝓝[Ici a] a
ha : ∃ b, a < b
b : α
hab : a < b
hbs : Ico a b ⊆ s
⊢ ∃ b, a ≤ b ∧ Icc a b ∈ 𝓝[Ici a] a ∧ Icc a b ⊆ s
case inr
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
hs : s ∈ 𝓝[Ici a] a
ha : ∃ b, a < b
⊢ ∃ b, a ≤ b ∧ Icc a b ∈ 𝓝[Ici a] a ∧ Icc a b ⊆ s
rcases(nhdsWithin_Ici_basis' ha).mem_iff.mp hs with ⟨b, hab, hbs⟩
case inr.intro.intro.inl
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
hs : s ∈ 𝓝[Ici a] a
ha : ∃ b, a < b
b : α
hab : a < b
hbs : Ico a b ⊆ s
H : Ioo a b = ∅
⊢ ∃ b, a ≤ b ∧ Icc a b ∈ 𝓝[Ici a] a ∧ Icc a b ⊆ s

case inr.intro.intro.inr.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
hs : s ∈ 𝓝[Ici a] a
ha : ∃ b, a < b
b : α
hab : a < b
hbs : Ico a b ⊆ s
c : α
hac : a < c
hcb : c < b
⊢ ∃ b, a ≤ b ∧ Icc a b ∈ 𝓝[Ici a] a ∧ Icc a b ⊆ s
case inr.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
hs : s ∈ 𝓝[Ici a] a
ha : ∃ b, a < b
b : α
hab : a < b
hbs : Ico a b ⊆ s
⊢ ∃ b, a ≤ b ∧ Icc a b ∈ 𝓝[Ici a] a ∧ Icc a b ⊆ s
rcases eq_empty_or_nonempty (Ioo a b) with (H | ⟨c, hac, hcb⟩)
case inr.intro.intro.inl
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
hs : s ∈ 𝓝[Ici a] a
ha : ∃ b, a < b
b : α
hab : a < b
hbs : Ico a b ⊆ s
H : Ioo a b = ∅
this : Ico a b = Icc a a
⊢ ∃ b, a ≤ b ∧ Icc a b ∈ 𝓝[Ici a] a ∧ Icc a b ⊆ s
case inr.intro.intro.inl
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
hs : s ∈ 𝓝[Ici a] a
ha : ∃ b, a < b
b : α
hab : a < b
hbs : Ico a b ⊆ s
H : Ioo a b = ∅
⊢ ∃ b, a ≤ b ∧ Icc a b ∈ 𝓝[Ici a] a ∧ Icc a b ⊆ s
have : Ico a b = Icc a a := by rw [← Icc_union_Ioo_eq_Ico le_rfl hab, H, union_empty]
no goals
case inr.intro.intro.inl
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
hs : s ∈ 𝓝[Ici a] a
ha : ∃ b, a < b
b : α
hab : a < b
hbs : Ico a b ⊆ s
H : Ioo a b = ∅
this : Ico a b = Icc a a
⊢ ∃ b, a ≤ b ∧ Icc a b ∈ 𝓝[Ici a] a ∧ Icc a b ⊆ s
exact ⟨a, le_rfl, this ▸ ⟨Ico_mem_nhdsWithin_Ici' hab, hbs⟩⟩
no goals
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
hs : s ∈ 𝓝[Ici a] a
ha : ∃ b, a < b
b : α
hab : a < b
hbs : Ico a b ⊆ s
H : Ioo a b = ∅
⊢ Ico a b = Icc a a
rw [← Icc_union_Ioo_eq_Ico le_rfl hab, H, union_empty]
case inr.intro.intro.inr.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
hs : s ∈ 𝓝[Ici a] a
ha : ∃ b, a < b
b : α
hab : a < b
hbs : Ico a b ⊆ s
c : α
hac : a < c
hcb : c < b
⊢ Icc a c ⊆ s
case inr.intro.intro.inr.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
hs : s ∈ 𝓝[Ici a] a
ha : ∃ b, a < b
b : α
hab : a < b
hbs : Ico a b ⊆ s
c : α
hac : a < c
hcb : c < b
⊢ ∃ b, a ≤ b ∧ Icc a b ∈ 𝓝[Ici a] a ∧ Icc a b ⊆ s
refine' ⟨c, hac.le, Icc_mem_nhdsWithin_Ici' hac, _⟩
no goals
case inr.intro.intro.inr.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
hs : s ∈ 𝓝[Ici a] a
ha : ∃ b, a < b
b : α
hab : a < b
hbs : Ico a b ⊆ s
c : α
hac : a < c
hcb : c < b
⊢ Icc a c ⊆ s
exact (Icc_subset_Ico_right hcb).trans hbs