α : Type u
β : Type v
γ : Type w
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : ConditionallyCompleteLinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : Nonempty γ
a b : α
s : Set α
hs : IsClosed (s ∩ Icc a b)
ha : a ∈ s
hgt : ∀ (x : α), x ∈ s ∩ Ico a b → ∀ (y : α), y ∈ Ioi x → Set.Nonempty (s ∩ Ioc x y)
y : α
hy : y ∈ Icc a b
⊢ y ∈ s
α : Type u
β : Type v
γ : Type w
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : ConditionallyCompleteLinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : Nonempty γ
a b : α
s : Set α
hs : IsClosed (s ∩ Icc a b)
ha : a ∈ s
hgt : ∀ (x : α), x ∈ s ∩ Ico a b → ∀ (y : α), y ∈ Ioi x → Set.Nonempty (s ∩ Ioc x y)
⊢ Icc a b ⊆ s
intro y hy
α : Type u
β : Type v
γ : Type w
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : ConditionallyCompleteLinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : Nonempty γ
a b : α
s : Set α
hs : IsClosed (s ∩ Icc a b)
ha : a ∈ s
hgt : ∀ (x : α), x ∈ s ∩ Ico a b → ∀ (y : α), y ∈ Ioi x → Set.Nonempty (s ∩ Ioc x y)
y : α
hy : y ∈ Icc a b
this : IsClosed (s ∩ Icc a y)
⊢ y ∈ s
α : Type u
β : Type v
γ : Type w
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : ConditionallyCompleteLinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : Nonempty γ
a b : α
s : Set α
hs : IsClosed (s ∩ Icc a b)
ha : a ∈ s
hgt : ∀ (x : α), x ∈ s ∩ Ico a b → ∀ (y : α), y ∈ Ioi x → Set.Nonempty (s ∩ Ioc x y)
y : α
hy : y ∈ Icc a b
⊢ y ∈ s
have : IsClosed (s ∩ Icc a y) := by
  suffices s ∩ Icc a y = s ∩ Icc a b ∩ Icc a y by
    rw [this]
    exact IsClosed.inter hs isClosed_Icc
  rw [inter_assoc]
  congr
  exact (inter_eq_self_of_subset_right <| Icc_subset_Icc_right hy.2).symm
no goals
α : Type u
β : Type v
γ : Type w
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : ConditionallyCompleteLinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : Nonempty γ
a b : α
s : Set α
hs : IsClosed (s ∩ Icc a b)
ha : a ∈ s
hgt : ∀ (x : α), x ∈ s ∩ Ico a b → ∀ (y : α), y ∈ Ioi x → Set.Nonempty (s ∩ Ioc x y)
y : α
hy : y ∈ Icc a b
this : IsClosed (s ∩ Icc a y)
⊢ y ∈ s
exact
  IsClosed.mem_of_ge_of_forall_exists_gt this ha hy.1 fun x hx =>
    hgt x ⟨hx.1, Ico_subset_Ico_right hy.2 hx.2⟩ y hx.2.2
α : Type u
β : Type v
γ : Type w
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : ConditionallyCompleteLinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : Nonempty γ
a b : α
s : Set α
hs : IsClosed (s ∩ Icc a b)
ha : a ∈ s
hgt : ∀ (x : α), x ∈ s ∩ Ico a b → ∀ (y : α), y ∈ Ioi x → Set.Nonempty (s ∩ Ioc x y)
y : α
hy : y ∈ Icc a b
⊢ s ∩ Icc a y = s ∩ Icc a b ∩ Icc a y
α : Type u
β : Type v
γ : Type w
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : ConditionallyCompleteLinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : Nonempty γ
a b : α
s : Set α
hs : IsClosed (s ∩ Icc a b)
ha : a ∈ s
hgt : ∀ (x : α), x ∈ s ∩ Ico a b → ∀ (y : α), y ∈ Ioi x → Set.Nonempty (s ∩ Ioc x y)
y : α
hy : y ∈ Icc a b
⊢ IsClosed (s ∩ Icc a y)
suffices s ∩ Icc a y = s ∩ Icc a b ∩ Icc a y by
  rw [this]
  exact IsClosed.inter hs isClosed_Icc
α : Type u
β : Type v
γ : Type w
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : ConditionallyCompleteLinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : Nonempty γ
a b : α
s : Set α
hs : IsClosed (s ∩ Icc a b)
ha : a ∈ s
hgt : ∀ (x : α), x ∈ s ∩ Ico a b → ∀ (y : α), y ∈ Ioi x → Set.Nonempty (s ∩ Ioc x y)
y : α
hy : y ∈ Icc a b
⊢ s ∩ Icc a y = s ∩ (Icc a b ∩ Icc a y)
α : Type u
β : Type v
γ : Type w
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : ConditionallyCompleteLinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : Nonempty γ
a b : α
s : Set α
hs : IsClosed (s ∩ Icc a b)
ha : a ∈ s
hgt : ∀ (x : α), x ∈ s ∩ Ico a b → ∀ (y : α), y ∈ Ioi x → Set.Nonempty (s ∩ Ioc x y)
y : α
hy : y ∈ Icc a b
⊢ s ∩ Icc a y = s ∩ Icc a b ∩ Icc a y
rw [inter_assoc]
case e_a
α : Type u
β : Type v
γ : Type w
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : ConditionallyCompleteLinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : Nonempty γ
a b : α
s : Set α
hs : IsClosed (s ∩ Icc a b)
ha : a ∈ s
hgt : ∀ (x : α), x ∈ s ∩ Ico a b → ∀ (y : α), y ∈ Ioi x → Set.Nonempty (s ∩ Ioc x y)
y : α
hy : y ∈ Icc a b
⊢ Icc a y = Icc a b ∩ Icc a y
α : Type u
β : Type v
γ : Type w
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : ConditionallyCompleteLinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : Nonempty γ
a b : α
s : Set α
hs : IsClosed (s ∩ Icc a b)
ha : a ∈ s
hgt : ∀ (x : α), x ∈ s ∩ Ico a b → ∀ (y : α), y ∈ Ioi x → Set.Nonempty (s ∩ Ioc x y)
y : α
hy : y ∈ Icc a b
⊢ s ∩ Icc a y = s ∩ (Icc a b ∩ Icc a y)
congr
no goals
case e_a
α : Type u
β : Type v
γ : Type w
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : ConditionallyCompleteLinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : Nonempty γ
a b : α
s : Set α
hs : IsClosed (s ∩ Icc a b)
ha : a ∈ s
hgt : ∀ (x : α), x ∈ s ∩ Ico a b → ∀ (y : α), y ∈ Ioi x → Set.Nonempty (s ∩ Ioc x y)
y : α
hy : y ∈ Icc a b
⊢ Icc a y = Icc a b ∩ Icc a y
exact (inter_eq_self_of_subset_right <| Icc_subset_Icc_right hy.2).symm
α : Type u
β : Type v
γ : Type w
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : ConditionallyCompleteLinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : Nonempty γ
a b : α
s : Set α
hs : IsClosed (s ∩ Icc a b)
ha : a ∈ s
hgt : ∀ (x : α), x ∈ s ∩ Ico a b → ∀ (y : α), y ∈ Ioi x → Set.Nonempty (s ∩ Ioc x y)
y : α
hy : y ∈ Icc a b
this : s ∩ Icc a y = s ∩ Icc a b ∩ Icc a y
⊢ IsClosed (s ∩ Icc a b ∩ Icc a y)
α : Type u
β : Type v
γ : Type w
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : ConditionallyCompleteLinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : Nonempty γ
a b : α
s : Set α
hs : IsClosed (s ∩ Icc a b)
ha : a ∈ s
hgt : ∀ (x : α), x ∈ s ∩ Ico a b → ∀ (y : α), y ∈ Ioi x → Set.Nonempty (s ∩ Ioc x y)
y : α
hy : y ∈ Icc a b
this : s ∩ Icc a y = s ∩ Icc a b ∩ Icc a y
⊢ IsClosed (s ∩ Icc a y)
rw [this]
no goals
α : Type u
β : Type v
γ : Type w
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : ConditionallyCompleteLinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : Nonempty γ
a b : α
s : Set α
hs : IsClosed (s ∩ Icc a b)
ha : a ∈ s
hgt : ∀ (x : α), x ∈ s ∩ Ico a b → ∀ (y : α), y ∈ Ioi x → Set.Nonempty (s ∩ Ioc x y)
y : α
hy : y ∈ Icc a b
this : s ∩ Icc a y = s ∩ Icc a b ∩ Icc a y
⊢ IsClosed (s ∩ Icc a b ∩ Icc a y)
exact IsClosed.inter hs isClosed_Icc