[GOAL]
α : Type ?u.6639
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : LowerTopology α
s : Set α
⊢ WithLowerTopology.instTopologicalSpaceWithLowerTopology = induced (↑WithLowerTopology.ofLower) inst✝¹
[PROOFSTEP]
erw [topology_eq α, induced_id]
[GOAL]
α : Type ?u.6639
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : LowerTopology α
s : Set α
⊢ WithLowerTopology.instTopologicalSpaceWithLowerTopology = generateFrom {s | ∃ a, (Ici a)ᶜ = s}
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : LowerTopology α
s : Set α
⊢ IsOpen s ↔ GenerateOpen {t | ∃ a, (Ici a)ᶜ = t} s
[PROOFSTEP]
rw [topology_eq α]
[GOAL]
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : LowerTopology α
s : Set α
⊢ IsOpen s ↔ GenerateOpen {t | ∃ a, (Ici a)ᶜ = t} s
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : LowerTopology α
s : Set α
h : Set.Finite s
⊢ IsClosed ↑(upperClosure s)
[PROOFSTEP]
simp only [← UpperSet.iInf_Ici, UpperSet.coe_iInf]
[GOAL]
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : LowerTopology α
s : Set α
h : Set.Finite s
⊢ IsClosed (⋃ (i : α) (_ : i ∈ s), ↑(UpperSet.Ici i))
[PROOFSTEP]
exact isClosed_biUnion h fun _ _ => isClosed_Ici
[GOAL]
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : LowerTopology α
s : Set α
h : IsOpen s
⊢ IsLowerSet s
[PROOFSTEP]
replace h := isOpen_iff_generate_Ici_compl.1 h
[GOAL]
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : LowerTopology α
s : Set α
h : GenerateOpen {t | ∃ a, (Ici a)ᶜ = t} s
⊢ IsLowerSet s
[PROOFSTEP]
induction h
[GOAL]
case basic
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : LowerTopology α
s s✝ : Set α
a✝ : s✝ ∈ {t | ∃ a, (Ici a)ᶜ = t}
⊢ IsLowerSet s✝
case univ
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : LowerTopology α
s : Set α
⊢ IsLowerSet univ
case inter
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : LowerTopology α
s s✝ t✝ : Set α
a✝¹ : GenerateOpen {t | ∃ a, (Ici a)ᶜ = t} s✝
a✝ : GenerateOpen {t | ∃ a, (Ici a)ᶜ = t} t✝
a_ih✝¹ : IsLowerSet s✝
a_ih✝ : IsLowerSet t✝
⊢ IsLowerSet (s✝ ∩ t✝)
case sUnion
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : LowerTopology α
s : Set α
S✝ : Set (Set α)
a✝ : ∀ (s : Set α), s ∈ S✝ → GenerateOpen {t | ∃ a, (Ici a)ᶜ = t} s
a_ih✝ : ∀ (s : Set α), s ∈ S✝ → IsLowerSet s
⊢ IsLowerSet (⋃₀ S✝)
[PROOFSTEP]
case basic u h' => obtain ⟨a, rfl⟩ := h'; exact (isUpperSet_Ici a).compl
[GOAL]
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : LowerTopology α
s u : Set α
h' : u ∈ {t | ∃ a, (Ici a)ᶜ = t}
⊢ IsLowerSet u
[PROOFSTEP]
case basic u h' => obtain ⟨a, rfl⟩ := h'; exact (isUpperSet_Ici a).compl
[GOAL]
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : LowerTopology α
s u : Set α
h' : u ∈ {t | ∃ a, (Ici a)ᶜ = t}
⊢ IsLowerSet u
[PROOFSTEP]
obtain ⟨a, rfl⟩ := h'
[GOAL]
case intro
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : LowerTopology α
s : Set α
a : α
⊢ IsLowerSet (Ici a)ᶜ
[PROOFSTEP]
exact (isUpperSet_Ici a).compl
[GOAL]
case univ
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : LowerTopology α
s : Set α
⊢ IsLowerSet univ
case inter
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : LowerTopology α
s s✝ t✝ : Set α
a✝¹ : GenerateOpen {t | ∃ a, (Ici a)ᶜ = t} s✝
a✝ : GenerateOpen {t | ∃ a, (Ici a)ᶜ = t} t✝
a_ih✝¹ : IsLowerSet s✝
a_ih✝ : IsLowerSet t✝
⊢ IsLowerSet (s✝ ∩ t✝)
case sUnion
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : LowerTopology α
s : Set α
S✝ : Set (Set α)
a✝ : ∀ (s : Set α), s ∈ S✝ → GenerateOpen {t | ∃ a, (Ici a)ᶜ = t} s
a_ih✝ : ∀ (s : Set α), s ∈ S✝ → IsLowerSet s
⊢ IsLowerSet (⋃₀ S✝)
[PROOFSTEP]
case univ => exact isLowerSet_univ
[GOAL]
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : LowerTopology α
s : Set α
⊢ IsLowerSet univ
[PROOFSTEP]
case univ => exact isLowerSet_univ
[GOAL]
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : LowerTopology α
s : Set α
⊢ IsLowerSet univ
[PROOFSTEP]
exact isLowerSet_univ
[GOAL]
case inter
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : LowerTopology α
s s✝ t✝ : Set α
a✝¹ : GenerateOpen {t | ∃ a, (Ici a)ᶜ = t} s✝
a✝ : GenerateOpen {t | ∃ a, (Ici a)ᶜ = t} t✝
a_ih✝¹ : IsLowerSet s✝
a_ih✝ : IsLowerSet t✝
⊢ IsLowerSet (s✝ ∩ t✝)
case sUnion
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : LowerTopology α
s : Set α
S✝ : Set (Set α)
a✝ : ∀ (s : Set α), s ∈ S✝ → GenerateOpen {t | ∃ a, (Ici a)ᶜ = t} s
a_ih✝ : ∀ (s : Set α), s ∈ S✝ → IsLowerSet s
⊢ IsLowerSet (⋃₀ S✝)
[PROOFSTEP]
case inter u v _ _ hu2 hv2 => exact hu2.inter hv2
[GOAL]
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : LowerTopology α
s u v : Set α
a✝¹ : GenerateOpen {t | ∃ a, (Ici a)ᶜ = t} u
a✝ : GenerateOpen {t | ∃ a, (Ici a)ᶜ = t} v
hu2 : IsLowerSet u
hv2 : IsLowerSet v
⊢ IsLowerSet (u ∩ v)
[PROOFSTEP]
case inter u v _ _ hu2 hv2 => exact hu2.inter hv2
[GOAL]
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : LowerTopology α
s u v : Set α
a✝¹ : GenerateOpen {t | ∃ a, (Ici a)ᶜ = t} u
a✝ : GenerateOpen {t | ∃ a, (Ici a)ᶜ = t} v
hu2 : IsLowerSet u
hv2 : IsLowerSet v
⊢ IsLowerSet (u ∩ v)
[PROOFSTEP]
exact hu2.inter hv2
[GOAL]
case sUnion
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : LowerTopology α
s : Set α
S✝ : Set (Set α)
a✝ : ∀ (s : Set α), s ∈ S✝ → GenerateOpen {t | ∃ a, (Ici a)ᶜ = t} s
a_ih✝ : ∀ (s : Set α), s ∈ S✝ → IsLowerSet s
⊢ IsLowerSet (⋃₀ S✝)
[PROOFSTEP]
case sUnion _ _ ih => exact isLowerSet_sUnion ih
[GOAL]
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : LowerTopology α
s : Set α
S✝ : Set (Set α)
a✝ : ∀ (s : Set α), s ∈ S✝ → GenerateOpen {t | ∃ a, (Ici a)ᶜ = t} s
ih : ∀ (s : Set α), s ∈ S✝ → IsLowerSet s
⊢ IsLowerSet (⋃₀ S✝)
[PROOFSTEP]
case sUnion _ _ ih => exact isLowerSet_sUnion ih
[GOAL]
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : LowerTopology α
s : Set α
S✝ : Set (Set α)
a✝ : ∀ (s : Set α), s ∈ S✝ → GenerateOpen {t | ∃ a, (Ici a)ᶜ = t} s
ih : ∀ (s : Set α), s ∈ S✝ → IsLowerSet s
⊢ IsLowerSet (⋃₀ S✝)
[PROOFSTEP]
exact isLowerSet_sUnion ih
[GOAL]
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : LowerTopology α
s : Set α
⊢ IsTopologicalBasis (lowerBasis α)
[PROOFSTEP]
convert isTopologicalBasis_of_subbasis (topology_eq α)
[GOAL]
case h.e'_3
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : LowerTopology α
s : Set α
⊢ lowerBasis α = (fun f => ⋂₀ f) '' {f | Set.Finite f ∧ f ⊆ {s | ∃ a, (Ici a)ᶜ = s}}
[PROOFSTEP]
simp_rw [lowerBasis, coe_upperClosure, compl_iUnion]
[GOAL]
case h.e'_3
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : LowerTopology α
s : Set α
⊢ {s | ∃ t, Set.Finite t ∧ ⋂ (i : α) (_ : i ∈ t), (Ici i)ᶜ = s} =
    (fun f => ⋂₀ f) '' {f | Set.Finite f ∧ f ⊆ {s | ∃ a, (Ici a)ᶜ = s}}
[PROOFSTEP]
ext s
[GOAL]
case h.e'_3.h
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : LowerTopology α
s✝ s : Set α
⊢ s ∈ {s | ∃ t, Set.Finite t ∧ ⋂ (i : α) (_ : i ∈ t), (Ici i)ᶜ = s} ↔
    s ∈ (fun f => ⋂₀ f) '' {f | Set.Finite f ∧ f ⊆ {s | ∃ a, (Ici a)ᶜ = s}}
[PROOFSTEP]
constructor
[GOAL]
case h.e'_3.h.mp
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : LowerTopology α
s✝ s : Set α
⊢ s ∈ {s | ∃ t, Set.Finite t ∧ ⋂ (i : α) (_ : i ∈ t), (Ici i)ᶜ = s} →
    s ∈ (fun f => ⋂₀ f) '' {f | Set.Finite f ∧ f ⊆ {s | ∃ a, (Ici a)ᶜ = s}}
[PROOFSTEP]
rintro ⟨F, hF, rfl⟩
[GOAL]
case h.e'_3.h.mp.intro.intro
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : LowerTopology α
s F : Set α
hF : Set.Finite F
⊢ ⋂ (i : α) (_ : i ∈ F), (Ici i)ᶜ ∈ (fun f => ⋂₀ f) '' {f | Set.Finite f ∧ f ⊆ {s | ∃ a, (Ici a)ᶜ = s}}
[PROOFSTEP]
refine' ⟨(fun a => (Ici a)ᶜ) '' F, ⟨hF.image _, image_subset_iff.2 fun _ _ => ⟨_, rfl⟩⟩, _⟩
[GOAL]
case h.e'_3.h.mp.intro.intro
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : LowerTopology α
s F : Set α
hF : Set.Finite F
⊢ (fun f => ⋂₀ f) ((fun a => (Ici a)ᶜ) '' F) = ⋂ (i : α) (_ : i ∈ F), (Ici i)ᶜ
[PROOFSTEP]
simp only [sInter_image]
[GOAL]
case h.e'_3.h.mpr
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : LowerTopology α
s✝ s : Set α
⊢ s ∈ (fun f => ⋂₀ f) '' {f | Set.Finite f ∧ f ⊆ {s | ∃ a, (Ici a)ᶜ = s}} →
    s ∈ {s | ∃ t, Set.Finite t ∧ ⋂ (i : α) (_ : i ∈ t), (Ici i)ᶜ = s}
[PROOFSTEP]
rintro ⟨F, ⟨hF, hs⟩, rfl⟩
[GOAL]
case h.e'_3.h.mpr.intro.intro.intro
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : LowerTopology α
s : Set α
F : Set (Set α)
hF : Set.Finite F
hs : F ⊆ {s | ∃ a, (Ici a)ᶜ = s}
⊢ (fun f => ⋂₀ f) F ∈ {s | ∃ t, Set.Finite t ∧ ⋂ (i : α) (_ : i ∈ t), (Ici i)ᶜ = s}
[PROOFSTEP]
haveI := hF.to_subtype
[GOAL]
case h.e'_3.h.mpr.intro.intro.intro
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : LowerTopology α
s : Set α
F : Set (Set α)
hF : Set.Finite F
hs : F ⊆ {s | ∃ a, (Ici a)ᶜ = s}
this : Finite ↑F
⊢ (fun f => ⋂₀ f) F ∈ {s | ∃ t, Set.Finite t ∧ ⋂ (i : α) (_ : i ∈ t), (Ici i)ᶜ = s}
[PROOFSTEP]
rw [subset_def, Subtype.forall'] at hs 
[GOAL]
case h.e'_3.h.mpr.intro.intro.intro
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : LowerTopology α
s : Set α
F : Set (Set α)
hF : Set.Finite F
hs : ∀ (x : { a // a ∈ F }), ↑x ∈ {s | ∃ a, (Ici a)ᶜ = s}
this : Finite ↑F
⊢ (fun f => ⋂₀ f) F ∈ {s | ∃ t, Set.Finite t ∧ ⋂ (i : α) (_ : i ∈ t), (Ici i)ᶜ = s}
[PROOFSTEP]
choose f hf using hs
[GOAL]
case h.e'_3.h.mpr.intro.intro.intro
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : LowerTopology α
s : Set α
F : Set (Set α)
hF : Set.Finite F
this : Finite ↑F
f : { a // a ∈ F } → α
hf : ∀ (x : { a // a ∈ F }), (Ici (f x))ᶜ = ↑x
⊢ (fun f => ⋂₀ f) F ∈ {s | ∃ t, Set.Finite t ∧ ⋂ (i : α) (_ : i ∈ t), (Ici i)ᶜ = s}
[PROOFSTEP]
exact ⟨_, finite_range f, by simp_rw [biInter_range, hf, sInter_eq_iInter]⟩
[GOAL]
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : LowerTopology α
s : Set α
F : Set (Set α)
hF : Set.Finite F
this : Finite ↑F
f : { a // a ∈ F } → α
hf : ∀ (x : { a // a ∈ F }), (Ici (f x))ᶜ = ↑x
⊢ ⋂ (i : α) (_ : i ∈ range f), (Ici i)ᶜ = (fun f => ⋂₀ f) F
[PROOFSTEP]
simp_rw [biInter_range, hf, sInter_eq_iInter]
[GOAL]
α : Type u_2
inst✝³ : Preorder α
inst✝² : TopologicalSpace α
inst✝¹ : LowerTopology α
s : Set α
β : Type u_1
inst✝ : TopologicalSpace β
f : β → α
h : ∀ (a : α), IsClosed (f ⁻¹' Ici a)
⊢ Continuous f
[PROOFSTEP]
obtain rfl := LowerTopology.topology_eq α
[GOAL]
α : Type u_2
inst✝² : Preorder α
s : Set α
β : Type u_1
inst✝¹ : TopologicalSpace β
f : β → α
h : ∀ (a : α), IsClosed (f ⁻¹' Ici a)
inst✝ : LowerTopology α
⊢ Continuous f
[PROOFSTEP]
refine continuous_generateFrom ?_
[GOAL]
α : Type u_2
inst✝² : Preorder α
s : Set α
β : Type u_1
inst✝¹ : TopologicalSpace β
f : β → α
h : ∀ (a : α), IsClosed (f ⁻¹' Ici a)
inst✝ : LowerTopology α
⊢ ∀ (s : Set α), s ∈ {s | ∃ a, (Ici a)ᶜ = s} → IsOpen (f ⁻¹' s)
[PROOFSTEP]
rintro _ ⟨a, rfl⟩
[GOAL]
case intro
α : Type u_2
inst✝² : Preorder α
s : Set α
β : Type u_1
inst✝¹ : TopologicalSpace β
f : β → α
h : ∀ (a : α), IsClosed (f ⁻¹' Ici a)
inst✝ : LowerTopology α
a : α
⊢ IsOpen (f ⁻¹' (Ici a)ᶜ)
[PROOFSTEP]
exact (h a).isOpen_compl
[GOAL]
α : Type ?u.15319
inst✝² : PartialOrder α
inst✝¹ : TopologicalSpace α
inst✝ : LowerTopology α
x y : α
h : Inseparable x y
⊢ Ici x = Ici y
[PROOFSTEP]
simpa only [inseparable_iff_closure_eq, closure_singleton] using h
[GOAL]
α : Type ?u.16169
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : UpperTopology α
s : Set α
⊢ WithUpperTopology.instTopologicalSpaceWithUpperTopology = induced (↑WithUpperTopology.ofUpper) inst✝¹
[PROOFSTEP]
erw [topology_eq α, induced_id]
[GOAL]
α : Type ?u.16169
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : UpperTopology α
s : Set α
⊢ WithUpperTopology.instTopologicalSpaceWithUpperTopology = generateFrom {s | ∃ a, (Iic a)ᶜ = s}
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : UpperTopology α
s : Set α
⊢ IsOpen s ↔ GenerateOpen {t | ∃ a, (Iic a)ᶜ = t} s
[PROOFSTEP]
rw [topology_eq α]
[GOAL]
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : UpperTopology α
s : Set α
⊢ IsOpen s ↔ GenerateOpen {t | ∃ a, (Iic a)ᶜ = t} s
[PROOFSTEP]
rfl
[GOAL]
α : Type ?u.18877
β : Type ?u.18906
inst✝⁷ : Preorder α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : LowerTopology α
inst✝⁴ : OrderBot α
inst✝³ : Preorder β
inst✝² : TopologicalSpace β
inst✝¹ : LowerTopology β
inst✝ : OrderBot β
⊢ instTopologicalSpaceProd = generateFrom {s | ∃ a, (Ici a)ᶜ = s}
[PROOFSTEP]
refine' le_antisymm (le_generateFrom _) _
[GOAL]
case refine'_1
α : Type ?u.18877
β : Type ?u.18906
inst✝⁷ : Preorder α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : LowerTopology α
inst✝⁴ : OrderBot α
inst✝³ : Preorder β
inst✝² : TopologicalSpace β
inst✝¹ : LowerTopology β
inst✝ : OrderBot β
⊢ ∀ (s : Set (α × β)), s ∈ {s | ∃ a, (Ici a)ᶜ = s} → IsOpen s
[PROOFSTEP]
rintro _ ⟨x, rfl⟩
[GOAL]
case refine'_1.intro
α : Type ?u.18877
β : Type ?u.18906
inst✝⁷ : Preorder α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : LowerTopology α
inst✝⁴ : OrderBot α
inst✝³ : Preorder β
inst✝² : TopologicalSpace β
inst✝¹ : LowerTopology β
inst✝ : OrderBot β
x : α × β
⊢ IsOpen (Ici x)ᶜ
[PROOFSTEP]
exact (isClosed_Ici.prod isClosed_Ici).isOpen_compl
[GOAL]
case refine'_2
α : Type ?u.18877
β : Type ?u.18906
inst✝⁷ : Preorder α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : LowerTopology α
inst✝⁴ : OrderBot α
inst✝³ : Preorder β
inst✝² : TopologicalSpace β
inst✝¹ : LowerTopology β
inst✝ : OrderBot β
⊢ generateFrom {s | ∃ a, (Ici a)ᶜ = s} ≤ instTopologicalSpaceProd
[PROOFSTEP]
rw [(LowerTopology.isTopologicalBasis.prod LowerTopology.isTopologicalBasis).eq_generateFrom,
  le_generateFrom_iff_subset_isOpen, image2_subset_iff]
[GOAL]
case refine'_2
α : Type ?u.18877
β : Type ?u.18906
inst✝⁷ : Preorder α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : LowerTopology α
inst✝⁴ : OrderBot α
inst✝³ : Preorder β
inst✝² : TopologicalSpace β
inst✝¹ : LowerTopology β
inst✝ : OrderBot β
⊢ ∀ (x : Set α),
    x ∈ LowerTopology.lowerBasis α → ∀ (y : Set β), y ∈ LowerTopology.lowerBasis β → x ×ˢ y ∈ {s | IsOpen s}
[PROOFSTEP]
rintro _ ⟨s, hs, rfl⟩ _ ⟨t, ht, rfl⟩
[GOAL]
case refine'_2.intro.intro.intro.intro
α : Type ?u.18877
β : Type ?u.18906
inst✝⁷ : Preorder α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : LowerTopology α
inst✝⁴ : OrderBot α
inst✝³ : Preorder β
inst✝² : TopologicalSpace β
inst✝¹ : LowerTopology β
inst✝ : OrderBot β
s : Set α
hs : Set.Finite s
t : Set β
ht : Set.Finite t
⊢ (↑(upperClosure s))ᶜ ×ˢ (↑(upperClosure t))ᶜ ∈ {s | IsOpen s}
[PROOFSTEP]
dsimp
[GOAL]
case refine'_2.intro.intro.intro.intro
α : Type ?u.18877
β : Type ?u.18906
inst✝⁷ : Preorder α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : LowerTopology α
inst✝⁴ : OrderBot α
inst✝³ : Preorder β
inst✝² : TopologicalSpace β
inst✝¹ : LowerTopology β
inst✝ : OrderBot β
s : Set α
hs : Set.Finite s
t : Set β
ht : Set.Finite t
⊢ IsOpen ((↑(upperClosure s))ᶜ ×ˢ (↑(upperClosure t))ᶜ)
[PROOFSTEP]
simp_rw [coe_upperClosure, compl_iUnion, prod_eq, preimage_iInter, preimage_compl]
  -- without `let`, `refine` tries to use the product topology and fails
[GOAL]
case refine'_2.intro.intro.intro.intro
α : Type ?u.18877
β : Type ?u.18906
inst✝⁷ : Preorder α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : LowerTopology α
inst✝⁴ : OrderBot α
inst✝³ : Preorder β
inst✝² : TopologicalSpace β
inst✝¹ : LowerTopology β
inst✝ : OrderBot β
s : Set α
hs : Set.Finite s
t : Set β
ht : Set.Finite t
⊢ IsOpen ((⋂ (i : α) (_ : i ∈ s), (Prod.fst ⁻¹' Ici i)ᶜ) ∩ ⋂ (i : β) (_ : i ∈ t), (Prod.snd ⁻¹' Ici i)ᶜ)
[PROOFSTEP]
let _ : TopologicalSpace (α × β) := generateFrom {s | ∃ a, (Ici a)ᶜ = s}
[GOAL]
case refine'_2.intro.intro.intro.intro
α : Type ?u.18877
β : Type ?u.18906
inst✝⁷ : Preorder α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : LowerTopology α
inst✝⁴ : OrderBot α
inst✝³ : Preorder β
inst✝² : TopologicalSpace β
inst✝¹ : LowerTopology β
inst✝ : OrderBot β
s : Set α
hs : Set.Finite s
t : Set β
ht : Set.Finite t
x✝ : TopologicalSpace (α × β) := generateFrom {s | ∃ a, (Ici a)ᶜ = s}
⊢ IsOpen ((⋂ (i : α) (_ : i ∈ s), (Prod.fst ⁻¹' Ici i)ᶜ) ∩ ⋂ (i : β) (_ : i ∈ t), (Prod.snd ⁻¹' Ici i)ᶜ)
[PROOFSTEP]
refine (isOpen_biInter hs fun a _ => ?_).inter (isOpen_biInter ht fun b _ => ?_)
[GOAL]
case refine'_2.intro.intro.intro.intro.refine_1
α : Type ?u.18877
β : Type ?u.18906
inst✝⁷ : Preorder α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : LowerTopology α
inst✝⁴ : OrderBot α
inst✝³ : Preorder β
inst✝² : TopologicalSpace β
inst✝¹ : LowerTopology β
inst✝ : OrderBot β
s : Set α
hs : Set.Finite s
t : Set β
ht : Set.Finite t
x✝¹ : TopologicalSpace (α × β) := generateFrom {s | ∃ a, (Ici a)ᶜ = s}
a : α
x✝ : a ∈ s
⊢ IsOpen (Prod.fst ⁻¹' Ici a)ᶜ
[PROOFSTEP]
exact GenerateOpen.basic _ ⟨(a, ⊥), by simp [Ici_prod_eq, prod_univ]⟩
[GOAL]
α : Type ?u.18877
β : Type ?u.18906
inst✝⁷ : Preorder α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : LowerTopology α
inst✝⁴ : OrderBot α
inst✝³ : Preorder β
inst✝² : TopologicalSpace β
inst✝¹ : LowerTopology β
inst✝ : OrderBot β
s : Set α
hs : Set.Finite s
t : Set β
ht : Set.Finite t
x✝¹ : TopologicalSpace (α × β) := generateFrom {s | ∃ a, (Ici a)ᶜ = s}
a : α
x✝ : a ∈ s
⊢ (Ici (a, ⊥))ᶜ = (Prod.fst ⁻¹' Ici a)ᶜ
[PROOFSTEP]
simp [Ici_prod_eq, prod_univ]
[GOAL]
case refine'_2.intro.intro.intro.intro.refine_2
α : Type ?u.18877
β : Type ?u.18906
inst✝⁷ : Preorder α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : LowerTopology α
inst✝⁴ : OrderBot α
inst✝³ : Preorder β
inst✝² : TopologicalSpace β
inst✝¹ : LowerTopology β
inst✝ : OrderBot β
s : Set α
hs : Set.Finite s
t : Set β
ht : Set.Finite t
x✝¹ : TopologicalSpace (α × β) := generateFrom {s | ∃ a, (Ici a)ᶜ = s}
b : β
x✝ : b ∈ t
⊢ IsOpen (Prod.snd ⁻¹' Ici b)ᶜ
[PROOFSTEP]
exact GenerateOpen.basic _ ⟨(⊥, b), by simp [Ici_prod_eq, univ_prod]⟩
[GOAL]
α : Type ?u.18877
β : Type ?u.18906
inst✝⁷ : Preorder α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : LowerTopology α
inst✝⁴ : OrderBot α
inst✝³ : Preorder β
inst✝² : TopologicalSpace β
inst✝¹ : LowerTopology β
inst✝ : OrderBot β
s : Set α
hs : Set.Finite s
t : Set β
ht : Set.Finite t
x✝¹ : TopologicalSpace (α × β) := generateFrom {s | ∃ a, (Ici a)ᶜ = s}
b : β
x✝ : b ∈ t
⊢ (Ici (⊥, b))ᶜ = (Prod.snd ⁻¹' Ici b)ᶜ
[PROOFSTEP]
simp [Ici_prod_eq, univ_prod]
[GOAL]
α : Type ?u.24860
β : Type ?u.24889
inst✝⁷ : Preorder α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : UpperTopology α
inst✝⁴ : OrderTop α
inst✝³ : Preorder β
inst✝² : TopologicalSpace β
inst✝¹ : UpperTopology β
inst✝ : OrderTop β
⊢ instTopologicalSpaceProd = generateFrom {s | ∃ a, (Iic a)ᶜ = s}
[PROOFSTEP]
suffices : LowerTopology (α × β)ᵒᵈ
[GOAL]
α : Type ?u.24860
β : Type ?u.24889
inst✝⁷ : Preorder α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : UpperTopology α
inst✝⁴ : OrderTop α
inst✝³ : Preorder β
inst✝² : TopologicalSpace β
inst✝¹ : UpperTopology β
inst✝ : OrderTop β
this : LowerTopology (α × β)ᵒᵈ
⊢ instTopologicalSpaceProd = generateFrom {s | ∃ a, (Iic a)ᶜ = s}
[PROOFSTEP]
exact LowerTopology.topology_eq_lowerTopology (α := (α × β)ᵒᵈ)
[GOAL]
case this
α : Type ?u.24860
β : Type ?u.24889
inst✝⁷ : Preorder α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : UpperTopology α
inst✝⁴ : OrderTop α
inst✝³ : Preorder β
inst✝² : TopologicalSpace β
inst✝¹ : UpperTopology β
inst✝ : OrderTop β
⊢ LowerTopology (α × β)ᵒᵈ
[PROOFSTEP]
exact instLowerTopologyProd (α := αᵒᵈ) (β := βᵒᵈ)
[GOAL]
α : Type u_2
β : Type u_1
inst✝⁵ : CompleteLattice α
inst✝⁴ : CompleteLattice β
inst✝³ : TopologicalSpace α
inst✝² : LowerTopology α
inst✝¹ : TopologicalSpace β
inst✝ : LowerTopology β
f : sInfHom α β
⊢ Continuous ↑f
[PROOFSTEP]
refine LowerTopology.continuous_of_Ici fun b => ?_
[GOAL]
α : Type u_2
β : Type u_1
inst✝⁵ : CompleteLattice α
inst✝⁴ : CompleteLattice β
inst✝³ : TopologicalSpace α
inst✝² : LowerTopology α
inst✝¹ : TopologicalSpace β
inst✝ : LowerTopology β
f : sInfHom α β
b : β
⊢ IsClosed (↑f ⁻¹' Ici b)
[PROOFSTEP]
convert isClosed_Ici (a := sInf <| f ⁻¹' Ici b)
[GOAL]
case h.e'_3
α : Type u_2
β : Type u_1
inst✝⁵ : CompleteLattice α
inst✝⁴ : CompleteLattice β
inst✝³ : TopologicalSpace α
inst✝² : LowerTopology α
inst✝¹ : TopologicalSpace β
inst✝ : LowerTopology β
f : sInfHom α β
b : β
⊢ ↑f ⁻¹' Ici b = Ici (sInf (↑f ⁻¹' Ici b))
[PROOFSTEP]
refine' Subset.antisymm (fun a => sInf_le) fun a ha => le_trans _ <| OrderHomClass.mono (f : α →o β) ha
[GOAL]
case h.e'_3
α : Type u_2
β : Type u_1
inst✝⁵ : CompleteLattice α
inst✝⁴ : CompleteLattice β
inst✝³ : TopologicalSpace α
inst✝² : LowerTopology α
inst✝¹ : TopologicalSpace β
inst✝ : LowerTopology β
f : sInfHom α β
b : β
a : α
ha : a ∈ Ici (sInf (↑f ⁻¹' Ici b))
⊢ b ≤ ↑↑f (sInf (↑f ⁻¹' Ici b))
[PROOFSTEP]
refine' LE.le.trans _ (map_sInf f _).ge
[GOAL]
case h.e'_3
α : Type u_2
β : Type u_1
inst✝⁵ : CompleteLattice α
inst✝⁴ : CompleteLattice β
inst✝³ : TopologicalSpace α
inst✝² : LowerTopology α
inst✝¹ : TopologicalSpace β
inst✝ : LowerTopology β
f : sInfHom α β
b : β
a : α
ha : a ∈ Ici (sInf (↑f ⁻¹' Ici b))
⊢ b ≤ sInf (↑f '' (↑f ⁻¹' Ici b))
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝¹ : Preorder α
inst✝ : TopologicalSpace α
⊢ UpperTopology αᵒᵈ ↔ LowerTopology α
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
inst✝¹ : Preorder α
inst✝ : TopologicalSpace α
⊢ UpperTopology αᵒᵈ → LowerTopology α
[PROOFSTEP]
apply UpperTopology.instLowerTopologyDual
[GOAL]
case mpr
α : Type u_1
inst✝¹ : Preorder α
inst✝ : TopologicalSpace α
⊢ LowerTopology α → UpperTopology αᵒᵈ
[PROOFSTEP]
apply LowerTopology.instUpperTopologyDual
[GOAL]
α : Type u_1
inst✝¹ : Preorder α
inst✝ : TopologicalSpace α
⊢ LowerTopology αᵒᵈ ↔ UpperTopology α
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
inst✝¹ : Preorder α
inst✝ : TopologicalSpace α
⊢ LowerTopology αᵒᵈ → UpperTopology α
[PROOFSTEP]
apply LowerTopology.instUpperTopologyDual
[GOAL]
case mpr
α : Type u_1
inst✝¹ : Preorder α
inst✝ : TopologicalSpace α
⊢ UpperTopology α → LowerTopology αᵒᵈ
[PROOFSTEP]
apply UpperTopology.instLowerTopologyDual
