α : Type u_1
inst✝ : OrderedCommGroup α
s t : Set α
a : α
hs : OrdConnected s
⊢ OrdConnected (a • ↑(upperClosure s) ∩ a • ↑(lowerClosure s))
α : Type u_1
inst✝ : OrderedCommGroup α
s t : Set α
a : α
hs : OrdConnected s
⊢ OrdConnected (a • s)
rw [← hs.upperClosure_inter_lowerClosure, smul_set_inter]
no goals
α : Type u_1
inst✝ : OrderedCommGroup α
s t : Set α
a : α
hs : OrdConnected s
⊢ OrdConnected (a • ↑(upperClosure s) ∩ a • ↑(lowerClosure s))
exact (upperClosure _).upper.smul.ordConnected.inter (lowerClosure _).lower.smul.ordConnected