case tfae_1_iff_2
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a b : α
hab : a < b
s : Set α
⊢ s ∈ 𝓝[Ici a] a ↔ s ∈ 𝓝[Icc a b] a

α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a b : α
hab : a < b
s : Set α
tfae_1_iff_2 : s ∈ 𝓝[Ici a] a ↔ s ∈ 𝓝[Icc a b] a
⊢ TFAE
    [s ∈ 𝓝[Ici a] a, s ∈ 𝓝[Icc a b] a, s ∈ 𝓝[Ico a b] a, ∃ u, u ∈ Ioc a b ∧ Ico a u ⊆ s, ∃ u, u ∈ Ioi a ∧ Ico a u ⊆ s]
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a b : α
hab : a < b
s : Set α
⊢ TFAE
    [s ∈ 𝓝[Ici a] a, s ∈ 𝓝[Icc a b] a, s ∈ 𝓝[Ico a b] a, ∃ u, u ∈ Ioc a b ∧ Ico a u ⊆ s, ∃ u, u ∈ Ioi a ∧ Ico a u ⊆ s]
tfae_have 1 ↔ 2
case tfae_1_iff_3
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a b : α
hab : a < b
s : Set α
tfae_1_iff_2 : s ∈ 𝓝[Ici a] a ↔ s ∈ 𝓝[Icc a b] a
⊢ s ∈ 𝓝[Ici a] a ↔ s ∈ 𝓝[Ico a b] a

α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a b : α
hab : a < b
s : Set α
tfae_1_iff_2 : s ∈ 𝓝[Ici a] a ↔ s ∈ 𝓝[Icc a b] a
tfae_1_iff_3 : s ∈ 𝓝[Ici a] a ↔ s ∈ 𝓝[Ico a b] a
⊢ TFAE
    [s ∈ 𝓝[Ici a] a, s ∈ 𝓝[Icc a b] a, s ∈ 𝓝[Ico a b] a, ∃ u, u ∈ Ioc a b ∧ Ico a u ⊆ s, ∃ u, u ∈ Ioi a ∧ Ico a u ⊆ s]
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a b : α
hab : a < b
s : Set α
tfae_1_iff_2 : s ∈ 𝓝[Ici a] a ↔ s ∈ 𝓝[Icc a b] a
⊢ TFAE
    [s ∈ 𝓝[Ici a] a, s ∈ 𝓝[Icc a b] a, s ∈ 𝓝[Ico a b] a, ∃ u, u ∈ Ioc a b ∧ Ico a u ⊆ s, ∃ u, u ∈ Ioi a ∧ Ico a u ⊆ s]
tfae_have 1 ↔ 3
case tfae_1_iff_5
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a b : α
hab : a < b
s : Set α
tfae_1_iff_2 : s ∈ 𝓝[Ici a] a ↔ s ∈ 𝓝[Icc a b] a
tfae_1_iff_3 : s ∈ 𝓝[Ici a] a ↔ s ∈ 𝓝[Ico a b] a
⊢ s ∈ 𝓝[Ici a] a ↔ ∃ u, u ∈ Ioi a ∧ Ico a u ⊆ s

α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a b : α
hab : a < b
s : Set α
tfae_1_iff_2 : s ∈ 𝓝[Ici a] a ↔ s ∈ 𝓝[Icc a b] a
tfae_1_iff_3 : s ∈ 𝓝[Ici a] a ↔ s ∈ 𝓝[Ico a b] a
tfae_1_iff_5 : s ∈ 𝓝[Ici a] a ↔ ∃ u, u ∈ Ioi a ∧ Ico a u ⊆ s
⊢ TFAE
    [s ∈ 𝓝[Ici a] a, s ∈ 𝓝[Icc a b] a, s ∈ 𝓝[Ico a b] a, ∃ u, u ∈ Ioc a b ∧ Ico a u ⊆ s, ∃ u, u ∈ Ioi a ∧ Ico a u ⊆ s]
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a b : α
hab : a < b
s : Set α
tfae_1_iff_2 : s ∈ 𝓝[Ici a] a ↔ s ∈ 𝓝[Icc a b] a
tfae_1_iff_3 : s ∈ 𝓝[Ici a] a ↔ s ∈ 𝓝[Ico a b] a
⊢ TFAE
    [s ∈ 𝓝[Ici a] a, s ∈ 𝓝[Icc a b] a, s ∈ 𝓝[Ico a b] a, ∃ u, u ∈ Ioc a b ∧ Ico a u ⊆ s, ∃ u, u ∈ Ioi a ∧ Ico a u ⊆ s]
tfae_have 1 ↔ 5
case tfae_4_to_5
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a b : α
hab : a < b
s : Set α
tfae_1_iff_2 : s ∈ 𝓝[Ici a] a ↔ s ∈ 𝓝[Icc a b] a
tfae_1_iff_3 : s ∈ 𝓝[Ici a] a ↔ s ∈ 𝓝[Ico a b] a
tfae_1_iff_5 : s ∈ 𝓝[Ici a] a ↔ ∃ u, u ∈ Ioi a ∧ Ico a u ⊆ s
⊢ (∃ u, u ∈ Ioc a b ∧ Ico a u ⊆ s) → ∃ u, u ∈ Ioi a ∧ Ico a u ⊆ s

α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a b : α
hab : a < b
s : Set α
tfae_1_iff_2 : s ∈ 𝓝[Ici a] a ↔ s ∈ 𝓝[Icc a b] a
tfae_1_iff_3 : s ∈ 𝓝[Ici a] a ↔ s ∈ 𝓝[Ico a b] a
tfae_1_iff_5 : s ∈ 𝓝[Ici a] a ↔ ∃ u, u ∈ Ioi a ∧ Ico a u ⊆ s
tfae_4_to_5 : (∃ u, u ∈ Ioc a b ∧ Ico a u ⊆ s) → ∃ u, u ∈ Ioi a ∧ Ico a u ⊆ s
⊢ TFAE
    [s ∈ 𝓝[Ici a] a, s ∈ 𝓝[Icc a b] a, s ∈ 𝓝[Ico a b] a, ∃ u, u ∈ Ioc a b ∧ Ico a u ⊆ s, ∃ u, u ∈ Ioi a ∧ Ico a u ⊆ s]
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a b : α
hab : a < b
s : Set α
tfae_1_iff_2 : s ∈ 𝓝[Ici a] a ↔ s ∈ 𝓝[Icc a b] a
tfae_1_iff_3 : s ∈ 𝓝[Ici a] a ↔ s ∈ 𝓝[Ico a b] a
tfae_1_iff_5 : s ∈ 𝓝[Ici a] a ↔ ∃ u, u ∈ Ioi a ∧ Ico a u ⊆ s
⊢ TFAE
    [s ∈ 𝓝[Ici a] a, s ∈ 𝓝[Icc a b] a, s ∈ 𝓝[Ico a b] a, ∃ u, u ∈ Ioc a b ∧ Ico a u ⊆ s, ∃ u, u ∈ Ioi a ∧ Ico a u ⊆ s]
tfae_have 4 → 5
case tfae_5_to_4
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a b : α
hab : a < b
s : Set α
tfae_1_iff_2 : s ∈ 𝓝[Ici a] a ↔ s ∈ 𝓝[Icc a b] a
tfae_1_iff_3 : s ∈ 𝓝[Ici a] a ↔ s ∈ 𝓝[Ico a b] a
tfae_1_iff_5 : s ∈ 𝓝[Ici a] a ↔ ∃ u, u ∈ Ioi a ∧ Ico a u ⊆ s
tfae_4_to_5 : (∃ u, u ∈ Ioc a b ∧ Ico a u ⊆ s) → ∃ u, u ∈ Ioi a ∧ Ico a u ⊆ s
⊢ (∃ u, u ∈ Ioi a ∧ Ico a u ⊆ s) → ∃ u, u ∈ Ioc a b ∧ Ico a u ⊆ s

α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a b : α
hab : a < b
s : Set α
tfae_1_iff_2 : s ∈ 𝓝[Ici a] a ↔ s ∈ 𝓝[Icc a b] a
tfae_1_iff_3 : s ∈ 𝓝[Ici a] a ↔ s ∈ 𝓝[Ico a b] a
tfae_1_iff_5 : s ∈ 𝓝[Ici a] a ↔ ∃ u, u ∈ Ioi a ∧ Ico a u ⊆ s
tfae_4_to_5 : (∃ u, u ∈ Ioc a b ∧ Ico a u ⊆ s) → ∃ u, u ∈ Ioi a ∧ Ico a u ⊆ s
tfae_5_to_4 : (∃ u, u ∈ Ioi a ∧ Ico a u ⊆ s) → ∃ u, u ∈ Ioc a b ∧ Ico a u ⊆ s
⊢ TFAE
    [s ∈ 𝓝[Ici a] a, s ∈ 𝓝[Icc a b] a, s ∈ 𝓝[Ico a b] a, ∃ u, u ∈ Ioc a b ∧ Ico a u ⊆ s, ∃ u, u ∈ Ioi a ∧ Ico a u ⊆ s]
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a b : α
hab : a < b
s : Set α
tfae_1_iff_2 : s ∈ 𝓝[Ici a] a ↔ s ∈ 𝓝[Icc a b] a
tfae_1_iff_3 : s ∈ 𝓝[Ici a] a ↔ s ∈ 𝓝[Ico a b] a
tfae_1_iff_5 : s ∈ 𝓝[Ici a] a ↔ ∃ u, u ∈ Ioi a ∧ Ico a u ⊆ s
tfae_4_to_5 : (∃ u, u ∈ Ioc a b ∧ Ico a u ⊆ s) → ∃ u, u ∈ Ioi a ∧ Ico a u ⊆ s
⊢ TFAE
    [s ∈ 𝓝[Ici a] a, s ∈ 𝓝[Icc a b] a, s ∈ 𝓝[Ico a b] a, ∃ u, u ∈ Ioc a b ∧ Ico a u ⊆ s, ∃ u, u ∈ Ioi a ∧ Ico a u ⊆ s]
tfae_have 5 → 4
no goals
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a b : α
hab : a < b
s : Set α
tfae_1_iff_2 : s ∈ 𝓝[Ici a] a ↔ s ∈ 𝓝[Icc a b] a
tfae_1_iff_3 : s ∈ 𝓝[Ici a] a ↔ s ∈ 𝓝[Ico a b] a
tfae_1_iff_5 : s ∈ 𝓝[Ici a] a ↔ ∃ u, u ∈ Ioi a ∧ Ico a u ⊆ s
tfae_4_to_5 : (∃ u, u ∈ Ioc a b ∧ Ico a u ⊆ s) → ∃ u, u ∈ Ioi a ∧ Ico a u ⊆ s
tfae_5_to_4 : (∃ u, u ∈ Ioi a ∧ Ico a u ⊆ s) → ∃ u, u ∈ Ioc a b ∧ Ico a u ⊆ s
⊢ TFAE
    [s ∈ 𝓝[Ici a] a, s ∈ 𝓝[Icc a b] a, s ∈ 𝓝[Ico a b] a, ∃ u, u ∈ Ioc a b ∧ Ico a u ⊆ s, ∃ u, u ∈ Ioi a ∧ Ico a u ⊆ s]
tfae_finish
no goals
case tfae_1_iff_2
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a b : α
hab : a < b
s : Set α
⊢ s ∈ 𝓝[Ici a] a ↔ s ∈ 𝓝[Icc a b] a
rw [nhdsWithin_Icc_eq_nhdsWithin_Ici hab]
no goals
case tfae_1_iff_3
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a b : α
hab : a < b
s : Set α
tfae_1_iff_2 : s ∈ 𝓝[Ici a] a ↔ s ∈ 𝓝[Icc a b] a
⊢ s ∈ 𝓝[Ici a] a ↔ s ∈ 𝓝[Ico a b] a
rw [nhdsWithin_Ico_eq_nhdsWithin_Ici hab]
no goals
case tfae_1_iff_5
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a b : α
hab : a < b
s : Set α
tfae_1_iff_2 : s ∈ 𝓝[Ici a] a ↔ s ∈ 𝓝[Icc a b] a
tfae_1_iff_3 : s ∈ 𝓝[Ici a] a ↔ s ∈ 𝓝[Ico a b] a
⊢ s ∈ 𝓝[Ici a] a ↔ ∃ u, u ∈ Ioi a ∧ Ico a u ⊆ s
exact (nhdsWithin_Ici_basis' ⟨b, hab⟩).mem_iff
no goals
case tfae_4_to_5
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a b : α
hab : a < b
s : Set α
tfae_1_iff_2 : s ∈ 𝓝[Ici a] a ↔ s ∈ 𝓝[Icc a b] a
tfae_1_iff_3 : s ∈ 𝓝[Ici a] a ↔ s ∈ 𝓝[Ico a b] a
tfae_1_iff_5 : s ∈ 𝓝[Ici a] a ↔ ∃ u, u ∈ Ioi a ∧ Ico a u ⊆ s
⊢ (∃ u, u ∈ Ioc a b ∧ Ico a u ⊆ s) → ∃ u, u ∈ Ioi a ∧ Ico a u ⊆ s
exact fun ⟨u, umem, hu⟩ => ⟨u, umem.1, hu⟩
case tfae_5_to_4.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a b : α
hab : a < b
s : Set α
tfae_1_iff_2 : s ∈ 𝓝[Ici a] a ↔ s ∈ 𝓝[Icc a b] a
tfae_1_iff_3 : s ∈ 𝓝[Ici a] a ↔ s ∈ 𝓝[Ico a b] a
tfae_1_iff_5 : s ∈ 𝓝[Ici a] a ↔ ∃ u, u ∈ Ioi a ∧ Ico a u ⊆ s
tfae_4_to_5 : (∃ u, u ∈ Ioc a b ∧ Ico a u ⊆ s) → ∃ u, u ∈ Ioi a ∧ Ico a u ⊆ s
u : α
hua : u ∈ Ioi a
hus : Ico a u ⊆ s
⊢ ∃ u, u ∈ Ioc a b ∧ Ico a u ⊆ s
case tfae_5_to_4
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a b : α
hab : a < b
s : Set α
tfae_1_iff_2 : s ∈ 𝓝[Ici a] a ↔ s ∈ 𝓝[Icc a b] a
tfae_1_iff_3 : s ∈ 𝓝[Ici a] a ↔ s ∈ 𝓝[Ico a b] a
tfae_1_iff_5 : s ∈ 𝓝[Ici a] a ↔ ∃ u, u ∈ Ioi a ∧ Ico a u ⊆ s
tfae_4_to_5 : (∃ u, u ∈ Ioc a b ∧ Ico a u ⊆ s) → ∃ u, u ∈ Ioi a ∧ Ico a u ⊆ s
⊢ (∃ u, u ∈ Ioi a ∧ Ico a u ⊆ s) → ∃ u, u ∈ Ioc a b ∧ Ico a u ⊆ s
rintro ⟨u, hua, hus⟩
no goals
case tfae_5_to_4.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a b : α
hab : a < b
s : Set α
tfae_1_iff_2 : s ∈ 𝓝[Ici a] a ↔ s ∈ 𝓝[Icc a b] a
tfae_1_iff_3 : s ∈ 𝓝[Ici a] a ↔ s ∈ 𝓝[Ico a b] a
tfae_1_iff_5 : s ∈ 𝓝[Ici a] a ↔ ∃ u, u ∈ Ioi a ∧ Ico a u ⊆ s
tfae_4_to_5 : (∃ u, u ∈ Ioc a b ∧ Ico a u ⊆ s) → ∃ u, u ∈ Ioi a ∧ Ico a u ⊆ s
u : α
hua : u ∈ Ioi a
hus : Ico a u ⊆ s
⊢ ∃ u, u ∈ Ioc a b ∧ Ico a u ⊆ s
exact
  ⟨min u b, ⟨lt_min hua hab, min_le_right _ _⟩,
    (Ico_subset_Ico_right <| min_le_left _ _).trans hus⟩