α : Type u
β : Type v
ι : Type ?u.10523
π : ι → Type ?u.10528
inst✝³ : TopologicalSpace α
s✝ t u v : Set α
inst✝² : LinearOrder β
inst✝¹ : SuccOrder β
inst✝ : IsSuccArchimedean β
s : β → Set α
H : ∀ (n : β), IsPreconnected (s n)
K : ∀ (n : β), Set.Nonempty (s n ∩ s (succ n))
i✝ j i : β
x✝ : i ∈ Ico j i✝
⊢ Set.Nonempty (s i ∩ s (succ i))
α : Type u
β : Type v
ι : Type ?u.10523
π : ι → Type ?u.10528
inst✝³ : TopologicalSpace α
s✝ t u v : Set α
inst✝² : LinearOrder β
inst✝¹ : SuccOrder β
inst✝ : IsSuccArchimedean β
s : β → Set α
H : ∀ (n : β), IsPreconnected (s n)
K : ∀ (n : β), Set.Nonempty (s n ∩ s (succ n))
i✝ j i : β
x✝ : i ∈ Ico j i✝
⊢ Set.Nonempty (s (succ i) ∩ s i)
rw [inter_comm]
no goals
α : Type u
β : Type v
ι : Type ?u.10523
π : ι → Type ?u.10528
inst✝³ : TopologicalSpace α
s✝ t u v : Set α
inst✝² : LinearOrder β
inst✝¹ : SuccOrder β
inst✝ : IsSuccArchimedean β
s : β → Set α
H : ∀ (n : β), IsPreconnected (s n)
K : ∀ (n : β), Set.Nonempty (s n ∩ s (succ n))
i✝ j i : β
x✝ : i ∈ Ico j i✝
⊢ Set.Nonempty (s i ∩ s (succ i))
exact K i