[GOAL]
α : Type u_1
β : Type u_2
inst✝ : Preorder α
⊢ UpperSetTopology α
[PROOFSTEP]
letI := upperSetTopology' α
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : Preorder α
this : TopologicalSpace α := upperSetTopology' α
⊢ UpperSetTopology α
[PROOFSTEP]
exact ⟨rfl⟩
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : Preorder α
⊢ LowerSetTopology α
[PROOFSTEP]
letI := lowerSetTopology' α
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : Preorder α
this : TopologicalSpace α := lowerSetTopology' α
⊢ LowerSetTopology α
[PROOFSTEP]
exact ⟨rfl⟩
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : TopologicalSpace α
inst✝³ : UpperSetTopology α
s : Set α
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : UpperSetTopology α
⊢ instTopologicalSpaceOrderDual = lowerSetTopology' αᵒᵈ
[PROOFSTEP]
refine topologicalSpace_eq ?_
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : TopologicalSpace α
inst✝³ : UpperSetTopology α
s : Set α
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : UpperSetTopology α
⊢ IsOpen = IsOpen
[PROOFSTEP]
rw [(UpperSetTopology.topology_eq (α))]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : UpperSetTopology α
s : Set α
⊢ WithUpperSetTopology.instTopologicalSpaceWithUpperSetTopology = induced (↑WithUpperSetTopology.ofUpperSet) inst✝¹
[PROOFSTEP]
erw [topology_eq α, induced_id]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : UpperSetTopology α
s : Set α
⊢ WithUpperSetTopology.instTopologicalSpaceWithUpperSetTopology = upperSetTopology' α
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : UpperSetTopology α
s : Set α
⊢ IsOpen s ↔ IsUpperSet s
[PROOFSTEP]
rw [topology_eq α]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : UpperSetTopology α
s : Set α
⊢ IsOpen s ↔ IsUpperSet s
[PROOFSTEP]
rfl
  -- Alexandrov property, set formulation
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : UpperSetTopology α
s : Set α
S : Set (Set α)
hf : ∀ (s : Set α), s ∈ S → IsOpen s
⊢ IsOpen (⋂₀ S)
[PROOFSTEP]
simp_rw [IsOpen_iff_IsUpperSet] at *
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : UpperSetTopology α
s : Set α
S : Set (Set α)
hf : ∀ (s : Set α), s ∈ S → IsUpperSet s
⊢ IsUpperSet (⋂₀ S)
[PROOFSTEP]
apply isUpperSet_sInter
[GOAL]
case hf
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : UpperSetTopology α
s : Set α
S : Set (Set α)
hf : ∀ (s : Set α), s ∈ S → IsUpperSet s
⊢ ∀ (s : Set α), s ∈ S → IsUpperSet s
[PROOFSTEP]
intros s hs
[GOAL]
case hf
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : UpperSetTopology α
s✝ : Set α
S : Set (Set α)
hf : ∀ (s : Set α), s ∈ S → IsUpperSet s
s : Set α
hs : s ∈ S
⊢ IsUpperSet s
[PROOFSTEP]
exact hf _ hs
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : UpperSetTopology α
s : Set α
ι : Sort u_3
f : ι → Set α
hf : ∀ (i : ι), IsOpen (f i)
⊢ IsOpen (⋂ (i : ι), f i)
[PROOFSTEP]
simp_rw [IsOpen_iff_IsUpperSet] at *
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : UpperSetTopology α
s : Set α
ι : Sort u_3
f : ι → Set α
hf : ∀ (i : ι), IsUpperSet (f i)
⊢ IsUpperSet (⋂ (i : ι), f i)
[PROOFSTEP]
apply isUpperSet_iInter
[GOAL]
case hf
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : UpperSetTopology α
s : Set α
ι : Sort u_3
f : ι → Set α
hf : ∀ (i : ι), IsUpperSet (f i)
⊢ ∀ (i : ι), IsUpperSet (f i)
[PROOFSTEP]
intros i
[GOAL]
case hf
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : UpperSetTopology α
s : Set α
ι : Sort u_3
f : ι → Set α
hf : ∀ (i : ι), IsUpperSet (f i)
i : ι
⊢ IsUpperSet (f i)
[PROOFSTEP]
exact hf i
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : UpperSetTopology α
s✝ s : Set α
⊢ IsClosed s ↔ IsLowerSet s
[PROOFSTEP]
rw [← isOpen_compl_iff, IsOpen_iff_IsUpperSet, isLowerSet_compl.symm, compl_compl]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : UpperSetTopology α
s✝ s : Set α
⊢ closure s = ↑(lowerClosure s)
[PROOFSTEP]
rw [subset_antisymm_iff]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : UpperSetTopology α
s✝ s : Set α
⊢ closure s ⊆ ↑(lowerClosure s) ∧ ↑(lowerClosure s) ⊆ closure s
[PROOFSTEP]
constructor
[GOAL]
case left
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : UpperSetTopology α
s✝ s : Set α
⊢ closure s ⊆ ↑(lowerClosure s)
[PROOFSTEP]
apply closure_minimal subset_lowerClosure _
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : UpperSetTopology α
s✝ s : Set α
⊢ IsClosed ↑(lowerClosure s)
[PROOFSTEP]
rw [isClosed_iff_isLower]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : UpperSetTopology α
s✝ s : Set α
⊢ IsLowerSet ↑(lowerClosure s)
[PROOFSTEP]
exact LowerSet.lower (lowerClosure s)
[GOAL]
case right
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : UpperSetTopology α
s✝ s : Set α
⊢ ↑(lowerClosure s) ⊆ closure s
[PROOFSTEP]
apply lowerClosure_min subset_closure (isClosed_isLower isClosed_closure)
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : UpperSetTopology α
s : Set α
a : α
⊢ closure {a} = Iic a
[PROOFSTEP]
rw [closure_eq_lowerClosure, lowerClosure_singleton]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : UpperSetTopology α
s : Set α
a : α
⊢ ↑(LowerSet.Iic a) = Iic a
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace α
inst✝² : UpperSetTopology α
inst✝¹ : TopologicalSpace β
inst✝ : UpperSetTopology β
f : α → β
⊢ Monotone f ↔ Continuous f
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace α
inst✝² : UpperSetTopology α
inst✝¹ : TopologicalSpace β
inst✝ : UpperSetTopology β
f : α → β
⊢ Monotone f → Continuous f
[PROOFSTEP]
intro hf
[GOAL]
case mp
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace α
inst✝² : UpperSetTopology α
inst✝¹ : TopologicalSpace β
inst✝ : UpperSetTopology β
f : α → β
hf : Monotone f
⊢ Continuous f
[PROOFSTEP]
simp_rw [continuous_def, IsOpen_iff_IsUpperSet]
[GOAL]
case mp
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace α
inst✝² : UpperSetTopology α
inst✝¹ : TopologicalSpace β
inst✝ : UpperSetTopology β
f : α → β
hf : Monotone f
⊢ ∀ (s : Set β), IsUpperSet s → IsUpperSet (f ⁻¹' s)
[PROOFSTEP]
exact fun _ hs ↦ IsUpperSet.preimage hs hf
[GOAL]
case mpr
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace α
inst✝² : UpperSetTopology α
inst✝¹ : TopologicalSpace β
inst✝ : UpperSetTopology β
f : α → β
⊢ Continuous f → Monotone f
[PROOFSTEP]
intro hf a b hab
[GOAL]
case mpr
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace α
inst✝² : UpperSetTopology α
inst✝¹ : TopologicalSpace β
inst✝ : UpperSetTopology β
f : α → β
hf : Continuous f
a b : α
hab : a ≤ b
⊢ f a ≤ f b
[PROOFSTEP]
rw [← mem_Iic, ← closure_singleton] at hab ⊢
[GOAL]
case mpr
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace α
inst✝² : UpperSetTopology α
inst✝¹ : TopologicalSpace β
inst✝ : UpperSetTopology β
f : α → β
hf : Continuous f
a b : α
hab✝ : a ∈ Iic b
hab : a ∈ closure {b}
⊢ f a ∈ closure {f b}
[PROOFSTEP]
apply (Continuous.closure_preimage_subset hf {f b})
[GOAL]
case mpr.a
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace α
inst✝² : UpperSetTopology α
inst✝¹ : TopologicalSpace β
inst✝ : UpperSetTopology β
f : α → β
hf : Continuous f
a b : α
hab✝ : a ∈ Iic b
hab : a ∈ closure {b}
⊢ a ∈ closure (f ⁻¹' {f b})
[PROOFSTEP]
apply mem_of_mem_of_subset hab
[GOAL]
case mpr.a
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace α
inst✝² : UpperSetTopology α
inst✝¹ : TopologicalSpace β
inst✝ : UpperSetTopology β
f : α → β
hf : Continuous f
a b : α
hab✝ : a ∈ Iic b
hab : a ∈ closure {b}
⊢ closure {b} ⊆ closure (f ⁻¹' {f b})
[PROOFSTEP]
apply closure_mono
[GOAL]
case mpr.a.h
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace α
inst✝² : UpperSetTopology α
inst✝¹ : TopologicalSpace β
inst✝ : UpperSetTopology β
f : α → β
hf : Continuous f
a b : α
hab✝ : a ∈ Iic b
hab : a ∈ closure {b}
⊢ {b} ⊆ f ⁻¹' {f b}
[PROOFSTEP]
rw [singleton_subset_iff, mem_preimage, mem_singleton_iff]
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace α
inst✝² : UpperSetTopology α
inst✝¹ : TopologicalSpace β
inst✝ : UpperTopology β
f : α → β
hf : Monotone f
⊢ Continuous f
[PROOFSTEP]
rw [continuous_def]
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace α
inst✝² : UpperSetTopology α
inst✝¹ : TopologicalSpace β
inst✝ : UpperTopology β
f : α → β
hf : Monotone f
⊢ ∀ (s : Set β), IsOpen s → IsOpen (f ⁻¹' s)
[PROOFSTEP]
intro s hs
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace α
inst✝² : UpperSetTopology α
inst✝¹ : TopologicalSpace β
inst✝ : UpperTopology β
f : α → β
hf : Monotone f
s : Set β
hs : IsOpen s
⊢ IsOpen (f ⁻¹' s)
[PROOFSTEP]
rw [IsOpen_iff_IsUpperSet]
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace α
inst✝² : UpperSetTopology α
inst✝¹ : TopologicalSpace β
inst✝ : UpperTopology β
f : α → β
hf : Monotone f
s : Set β
hs : IsOpen s
⊢ IsUpperSet (f ⁻¹' s)
[PROOFSTEP]
apply IsUpperSet.preimage _ hf
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace α
inst✝² : UpperSetTopology α
inst✝¹ : TopologicalSpace β
inst✝ : UpperTopology β
f : α → β
hf : Monotone f
s : Set β
hs : IsOpen s
⊢ IsUpperSet s
[PROOFSTEP]
apply UpperTopology.isUpperSet_of_isOpen hs
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
t₁ : TopologicalSpace α
inst✝¹ : UpperSetTopology α
t₂ : TopologicalSpace α
inst✝ : UpperTopology α
s : Set α
hs : IsOpen s
⊢ IsOpen s
[PROOFSTEP]
rw [@IsOpen_iff_IsUpperSet α _ t₁]
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
t₁ : TopologicalSpace α
inst✝¹ : UpperSetTopology α
t₂ : TopologicalSpace α
inst✝ : UpperTopology α
s : Set α
hs : IsOpen s
⊢ IsUpperSet s
[PROOFSTEP]
exact UpperTopology.isUpperSet_of_isOpen hs
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : TopologicalSpace α
inst✝³ : LowerSetTopology α
s : Set α
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : LowerSetTopology α
⊢ instTopologicalSpaceOrderDual = upperSetTopology' αᵒᵈ
[PROOFSTEP]
refine topologicalSpace_eq ?_
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : TopologicalSpace α
inst✝³ : LowerSetTopology α
s : Set α
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : LowerSetTopology α
⊢ IsOpen = IsOpen
[PROOFSTEP]
rw [(LowerSetTopology.topology_eq (α))]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : LowerSetTopology α
s : Set α
⊢ WithLowerSetTopology.instTopologicalSpaceWithLowerSetTopology = induced (↑WithLowerSetTopology.ofLowerSet) inst✝¹
[PROOFSTEP]
erw [topology_eq α, induced_id]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : LowerSetTopology α
s : Set α
⊢ WithLowerSetTopology.instTopologicalSpaceWithLowerSetTopology = lowerSetTopology' α
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : LowerSetTopology α
s : Set α
⊢ IsOpen s ↔ IsLowerSet s
[PROOFSTEP]
rw [topology_eq α]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : LowerSetTopology α
s : Set α
⊢ IsOpen s ↔ IsLowerSet s
[PROOFSTEP]
rfl
  -- Alexandrov property, set formulation
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : LowerSetTopology α
s✝ s : Set α
⊢ IsClosed s ↔ IsUpperSet s
[PROOFSTEP]
rw [← isOpen_compl_iff, IsOpen_iff_IsLowerSet, isUpperSet_compl.symm, compl_compl]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : LowerSetTopology α
s : Set α
a : α
⊢ closure {a} = Ici a
[PROOFSTEP]
rw [closure_eq_upperClosure, upperClosure_singleton]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : LowerSetTopology α
s : Set α
a : α
⊢ ↑(UpperSet.Ici a) = Ici a
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace α
inst✝² : LowerSetTopology α
inst✝¹ : TopologicalSpace β
inst✝ : LowerSetTopology β
f : α → β
⊢ Monotone f ↔ Continuous f
[PROOFSTEP]
rw [← monotone_dual_iff]
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace α
inst✝² : LowerSetTopology α
inst✝¹ : TopologicalSpace β
inst✝ : LowerSetTopology β
f : α → β
⊢ Monotone (↑toDual ∘ f ∘ ↑ofDual) ↔ Continuous f
[PROOFSTEP]
exact UpperSetTopology.monotone_iff_continuous (α := αᵒᵈ) (β := βᵒᵈ) (f := (toDual ∘ f ∘ ofDual : αᵒᵈ → βᵒᵈ))
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace α
inst✝² : LowerSetTopology α
inst✝¹ : TopologicalSpace β
inst✝ : LowerTopology β
f : α → β
hf : Monotone f
⊢ Continuous f
[PROOFSTEP]
apply
  UpperSetTopology.Monotone_to_UpperTopology_Continuous (α := αᵒᵈ) (β := βᵒᵈ) (f := (toDual ∘ f ∘ ofDual : αᵒᵈ → βᵒᵈ))
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace α
inst✝² : LowerSetTopology α
inst✝¹ : TopologicalSpace β
inst✝ : LowerTopology β
f : α → β
hf : Monotone f
⊢ Monotone (↑toDual ∘ f ∘ ↑ofDual)
[PROOFSTEP]
exact Monotone.dual hf
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
t₁ : TopologicalSpace α
inst✝¹ : LowerSetTopology α
t₂ : TopologicalSpace α
inst✝ : LowerTopology α
s : Set α
hs : IsOpen s
⊢ IsOpen s
[PROOFSTEP]
rw [@IsOpen_iff_IsLowerSet α _ t₁]
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
t₁ : TopologicalSpace α
inst✝¹ : LowerSetTopology α
t₂ : TopologicalSpace α
inst✝ : LowerTopology α
s : Set α
hs : IsOpen s
⊢ IsLowerSet s
[PROOFSTEP]
exact LowerTopology.isLowerSet_of_isOpen hs
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : TopologicalSpace α
⊢ UpperSetTopology αᵒᵈ ↔ LowerSetTopology α
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : TopologicalSpace α
⊢ UpperSetTopology αᵒᵈ → LowerSetTopology α
[PROOFSTEP]
apply UpperSetTopology.instLowerSetTopologyDual
[GOAL]
case mpr
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : TopologicalSpace α
⊢ LowerSetTopology α → UpperSetTopology αᵒᵈ
[PROOFSTEP]
apply LowerSetTopology.instUpperSetTopologyDual
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : TopologicalSpace α
⊢ LowerSetTopology αᵒᵈ ↔ UpperSetTopology α
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : TopologicalSpace α
⊢ LowerSetTopology αᵒᵈ → UpperSetTopology α
[PROOFSTEP]
apply LowerSetTopology.instUpperSetTopologyDual
[GOAL]
case mpr
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : TopologicalSpace α
⊢ UpperSetTopology α → LowerSetTopology αᵒᵈ
[PROOFSTEP]
apply UpperSetTopology.instLowerSetTopologyDual
