α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : SuccOrder α
a : α
⊢ IsOpen {a}
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : SuccOrder α
⊢ ⊥ = generateFrom {s | ∃ a, s = Ioi a ∨ s = Iio a}
refine' (eq_bot_of_singletons_open fun a => _).symm
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : SuccOrder α
a : α
h_singleton_eq_inter : {a} = Iic a ∩ Ici a
⊢ IsOpen {a}
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : SuccOrder α
a : α
⊢ IsOpen {a}
have h_singleton_eq_inter : {a} = Iic a ∩ Ici a := by rw [inter_comm, Ici_inter_Iic, Icc_self a]
case pos
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : SuccOrder α
a : α
h_singleton_eq_inter : {a} = Iic a ∩ Ici a
ha_top : IsTop a
⊢ IsOpen {a}

case neg
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : SuccOrder α
a : α
h_singleton_eq_inter : {a} = Iic a ∩ Ici a
ha_top : ¬IsTop a
⊢ IsOpen {a}
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : SuccOrder α
a : α
h_singleton_eq_inter : {a} = Iic a ∩ Ici a
⊢ IsOpen {a}
by_cases ha_top : IsTop a
no goals
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : SuccOrder α
a : α
⊢ {a} = Iic a ∩ Ici a
rw [inter_comm, Ici_inter_Iic, Icc_self a]
case pos
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : SuccOrder α
a : α
h_singleton_eq_inter : {a} = Ici a
ha_top : IsTop a
⊢ IsOpen {a}
case pos
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : SuccOrder α
a : α
h_singleton_eq_inter : {a} = Iic a ∩ Ici a
ha_top : IsTop a
⊢ IsOpen {a}
rw [ha_top.Iic_eq, inter_comm, inter_univ] at h_singleton_eq_inter
case pos
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : SuccOrder α
a : α
h_singleton_eq_inter : {a} = Ici a
ha_top : IsTop a
ha_bot : IsBot a
⊢ IsOpen {a}

case neg
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : SuccOrder α
a : α
h_singleton_eq_inter : {a} = Ici a
ha_top : IsTop a
ha_bot : ¬IsBot a
⊢ IsOpen {a}
case pos
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : SuccOrder α
a : α
h_singleton_eq_inter : {a} = Ici a
ha_top : IsTop a
⊢ IsOpen {a}
by_cases ha_bot : IsBot a
case pos
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : SuccOrder α
a : α
h_singleton_eq_inter : {a} = univ
ha_top : IsTop a
ha_bot : IsBot a
⊢ IsOpen {a}
case pos
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : SuccOrder α
a : α
h_singleton_eq_inter : {a} = Ici a
ha_top : IsTop a
ha_bot : IsBot a
⊢ IsOpen {a}
rw [ha_bot.Ici_eq] at h_singleton_eq_inter
case pos
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : SuccOrder α
a : α
h_singleton_eq_inter : {a} = univ
ha_top : IsTop a
ha_bot : IsBot a
⊢ IsOpen univ
case pos
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : SuccOrder α
a : α
h_singleton_eq_inter : {a} = univ
ha_top : IsTop a
ha_bot : IsBot a
⊢ IsOpen {a}
rw [h_singleton_eq_inter]
no goals
case pos
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : SuccOrder α
a : α
h_singleton_eq_inter : {a} = univ
ha_top : IsTop a
ha_bot : IsBot a
⊢ IsOpen univ
apply @isOpen_univ _ (generateFrom { s | ∃ a, s = Ioi a ∨ s = Iio a })
case neg
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : SuccOrder α
a : α
h_singleton_eq_inter : {a} = Ici a
ha_top : IsTop a
ha_bot : ¬IsMin a
⊢ IsOpen {a}
case neg
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : SuccOrder α
a : α
h_singleton_eq_inter : {a} = Ici a
ha_top : IsTop a
ha_bot : ¬IsBot a
⊢ IsOpen {a}
rw [isBot_iff_isMin] at ha_bot
case neg
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : SuccOrder α
a : α
h_singleton_eq_inter : {a} = Ioi (pred a)
ha_top : IsTop a
ha_bot : ¬IsMin a
⊢ IsOpen {a}
case neg
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : SuccOrder α
a : α
h_singleton_eq_inter : {a} = Ici a
ha_top : IsTop a
ha_bot : ¬IsMin a
⊢ IsOpen {a}
rw [← Ioi_pred_of_not_isMin ha_bot] at h_singleton_eq_inter
case neg
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : SuccOrder α
a : α
h_singleton_eq_inter : {a} = Ioi (pred a)
ha_top : IsTop a
ha_bot : ¬IsMin a
⊢ IsOpen (Ioi (pred a))
case neg
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : SuccOrder α
a : α
h_singleton_eq_inter : {a} = Ioi (pred a)
ha_top : IsTop a
ha_bot : ¬IsMin a
⊢ IsOpen {a}
rw [h_singleton_eq_inter]
no goals
case neg
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : SuccOrder α
a : α
h_singleton_eq_inter : {a} = Ioi (pred a)
ha_top : IsTop a
ha_bot : ¬IsMin a
⊢ IsOpen (Ioi (pred a))
exact isOpen_generateFrom_of_mem ⟨pred a, Or.inl rfl⟩
case neg
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : SuccOrder α
a : α
h_singleton_eq_inter : {a} = Iic a ∩ Ici a
ha_top : ¬IsMax a
⊢ IsOpen {a}
case neg
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : SuccOrder α
a : α
h_singleton_eq_inter : {a} = Iic a ∩ Ici a
ha_top : ¬IsTop a
⊢ IsOpen {a}
rw [isTop_iff_isMax] at ha_top
case neg
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : SuccOrder α
a : α
h_singleton_eq_inter : {a} = Iio (succ a) ∩ Ici a
ha_top : ¬IsMax a
⊢ IsOpen {a}
case neg
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : SuccOrder α
a : α
h_singleton_eq_inter : {a} = Iic a ∩ Ici a
ha_top : ¬IsMax a
⊢ IsOpen {a}
rw [← Iio_succ_of_not_isMax ha_top] at h_singleton_eq_inter
case pos
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : SuccOrder α
a : α
h_singleton_eq_inter : {a} = Iio (succ a) ∩ Ici a
ha_top : ¬IsMax a
ha_bot : IsBot a
⊢ IsOpen {a}

case neg
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : SuccOrder α
a : α
h_singleton_eq_inter : {a} = Iio (succ a) ∩ Ici a
ha_top : ¬IsMax a
ha_bot : ¬IsBot a
⊢ IsOpen {a}
case neg
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : SuccOrder α
a : α
h_singleton_eq_inter : {a} = Iio (succ a) ∩ Ici a
ha_top : ¬IsMax a
⊢ IsOpen {a}
by_cases ha_bot : IsBot a
case pos
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : SuccOrder α
a : α
h_singleton_eq_inter : {a} = Iio (succ a)
ha_top : ¬IsMax a
ha_bot : IsBot a
⊢ IsOpen {a}
case pos
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : SuccOrder α
a : α
h_singleton_eq_inter : {a} = Iio (succ a) ∩ Ici a
ha_top : ¬IsMax a
ha_bot : IsBot a
⊢ IsOpen {a}
rw [ha_bot.Ici_eq, inter_univ] at h_singleton_eq_inter
case pos
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : SuccOrder α
a : α
h_singleton_eq_inter : {a} = Iio (succ a)
ha_top : ¬IsMax a
ha_bot : IsBot a
⊢ IsOpen (Iio (succ a))
case pos
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : SuccOrder α
a : α
h_singleton_eq_inter : {a} = Iio (succ a)
ha_top : ¬IsMax a
ha_bot : IsBot a
⊢ IsOpen {a}
rw [h_singleton_eq_inter]
no goals
case pos
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : SuccOrder α
a : α
h_singleton_eq_inter : {a} = Iio (succ a)
ha_top : ¬IsMax a
ha_bot : IsBot a
⊢ IsOpen (Iio (succ a))
exact isOpen_generateFrom_of_mem ⟨succ a, Or.inr rfl⟩
case neg
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : SuccOrder α
a : α
h_singleton_eq_inter : {a} = Iio (succ a) ∩ Ici a
ha_top : ¬IsMax a
ha_bot : ¬IsMin a
⊢ IsOpen {a}
case neg
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : SuccOrder α
a : α
h_singleton_eq_inter : {a} = Iio (succ a) ∩ Ici a
ha_top : ¬IsMax a
ha_bot : ¬IsBot a
⊢ IsOpen {a}
rw [isBot_iff_isMin] at ha_bot
case neg
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : SuccOrder α
a : α
h_singleton_eq_inter : {a} = Iio (succ a) ∩ Ioi (pred a)
ha_top : ¬IsMax a
ha_bot : ¬IsMin a
⊢ IsOpen {a}
case neg
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : SuccOrder α
a : α
h_singleton_eq_inter : {a} = Iio (succ a) ∩ Ici a
ha_top : ¬IsMax a
ha_bot : ¬IsMin a
⊢ IsOpen {a}
rw [← Ioi_pred_of_not_isMin ha_bot] at h_singleton_eq_inter
case neg
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : SuccOrder α
a : α
h_singleton_eq_inter : {a} = Iio (succ a) ∩ Ioi (pred a)
ha_top : ¬IsMax a
ha_bot : ¬IsMin a
⊢ IsOpen (Iio (succ a) ∩ Ioi (pred a))
case neg
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : SuccOrder α
a : α
h_singleton_eq_inter : {a} = Iio (succ a) ∩ Ioi (pred a)
ha_top : ¬IsMax a
ha_bot : ¬IsMin a
⊢ IsOpen {a}
rw [h_singleton_eq_inter]
case neg.h₁
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : SuccOrder α
a : α
h_singleton_eq_inter : {a} = Iio (succ a) ∩ Ioi (pred a)
ha_top : ¬IsMax a
ha_bot : ¬IsMin a
⊢ IsOpen (Iio (succ a))

case neg.h₂
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : SuccOrder α
a : α
h_singleton_eq_inter : {a} = Iio (succ a) ∩ Ioi (pred a)
ha_top : ¬IsMax a
ha_bot : ¬IsMin a
⊢ IsOpen (Ioi (pred a))
case neg
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : SuccOrder α
a : α
h_singleton_eq_inter : {a} = Iio (succ a) ∩ Ioi (pred a)
ha_top : ¬IsMax a
ha_bot : ¬IsMin a
⊢ IsOpen (Iio (succ a) ∩ Ioi (pred a))
apply @IsOpen.inter _ _ _ (generateFrom { s | ∃ a, s = Ioi a ∨ s = Iio a })
no goals
case neg.h₁
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : SuccOrder α
a : α
h_singleton_eq_inter : {a} = Iio (succ a) ∩ Ioi (pred a)
ha_top : ¬IsMax a
ha_bot : ¬IsMin a
⊢ IsOpen (Iio (succ a))
exact isOpen_generateFrom_of_mem ⟨succ a, Or.inr rfl⟩
no goals
case neg.h₂
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : SuccOrder α
a : α
h_singleton_eq_inter : {a} = Iio (succ a) ∩ Ioi (pred a)
ha_top : ¬IsMax a
ha_bot : ¬IsMin a
⊢ IsOpen (Ioi (pred a))
exact isOpen_generateFrom_of_mem ⟨pred a, Or.inl rfl⟩