[GOAL]
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : OrderedCommGroup α
inst✝ : ContinuousConstSMul α α
s : Set α
h : IsUpperSet s
x y : α
hxy : x ≤ y
hx : x ∈ closure s
⊢ y ∈ closure ((y / x) • s)
[PROOFSTEP]
rw [closure_smul]
[GOAL]
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : OrderedCommGroup α
inst✝ : ContinuousConstSMul α α
s : Set α
h : IsUpperSet s
x y : α
hxy : x ≤ y
hx : x ∈ closure s
⊢ y ∈ (y / x) • closure s
[PROOFSTEP]
exact ⟨x, hx, div_mul_cancel' _ _⟩
[GOAL]
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : OrderedCommGroup α
inst✝ : ContinuousConstSMul α α
s : Set α
h : IsLowerSet s
x y : α
hxy : y ≤ x
hx : x ∈ closure s
⊢ y ∈ closure ((y / x) • s)
[PROOFSTEP]
rw [closure_smul]
[GOAL]
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : OrderedCommGroup α
inst✝ : ContinuousConstSMul α α
s : Set α
h : IsLowerSet s
x y : α
hxy : y ≤ x
hx : x ∈ closure s
⊢ y ∈ (y / x) • closure s
[PROOFSTEP]
exact ⟨x, hx, div_mul_cancel' _ _⟩
[GOAL]
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : OrderedCommGroup α
inst✝ : ContinuousConstSMul α α
s : Set α
hs : IsOpen s
⊢ IsOpen ↑(upperClosure s)
[PROOFSTEP]
rw [← mul_one s, ← mul_upperClosure]
[GOAL]
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : OrderedCommGroup α
inst✝ : ContinuousConstSMul α α
s : Set α
hs : IsOpen s
⊢ IsOpen (s * ↑(upperClosure 1))
[PROOFSTEP]
exact hs.mul_right
[GOAL]
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : OrderedCommGroup α
inst✝ : ContinuousConstSMul α α
s : Set α
hs : IsOpen s
⊢ IsOpen ↑(lowerClosure s)
[PROOFSTEP]
rw [← mul_one s, ← mul_lowerClosure]
[GOAL]
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : OrderedCommGroup α
inst✝ : ContinuousConstSMul α α
s : Set α
hs : IsOpen s
⊢ IsOpen (s * ↑(lowerClosure 1))
[PROOFSTEP]
exact hs.mul_right
[GOAL]
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : HasUpperLowerClosure α
s : Set α
h : IsUpperSet s
⊢ IsUpperSet (interior s)
[PROOFSTEP]
rw [← isLowerSet_compl, ← closure_compl]
[GOAL]
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : HasUpperLowerClosure α
s : Set α
h : IsUpperSet s
⊢ IsLowerSet (closure sᶜ)
[PROOFSTEP]
exact h.compl.closure
[GOAL]
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : HasUpperLowerClosure α
s : Set α
h : OrdConnected s
⊢ OrdConnected (interior s)
[PROOFSTEP]
rw [← h.upperClosure_inter_lowerClosure, interior_inter]
[GOAL]
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : HasUpperLowerClosure α
s : Set α
h : OrdConnected s
⊢ OrdConnected (interior ↑(upperClosure s) ∩ interior ↑(lowerClosure s))
[PROOFSTEP]
exact (upperClosure s).upper.interior.ordConnected.inter (lowerClosure s).lower.interior.ordConnected
