case h.e'_3
α : Type u_1
β : Type ?u.6266
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : LowerTopology α
s : Set α
⊢ lowerBasis α = (fun f => ⋂₀ f) '' {f | Set.Finite f ∧ f ⊆ {s | ∃ a, Ici aᶜ = s}}
α : Type u_1
β : Type ?u.6266
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : LowerTopology α
s : Set α
⊢ IsTopologicalBasis (lowerBasis α)
convert isTopologicalBasis_of_subbasis (topology_eq α)
case h.e'_3
α : Type u_1
β : Type ?u.6266
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}}
case h.e'_3
α : Type u_1
β : Type ?u.6266
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : LowerTopology α
s : Set α
⊢ lowerBasis α = (fun f => ⋂₀ f) '' {f | Set.Finite f ∧ f ⊆ {s | ∃ a, Ici aᶜ = s}}
simp_rw [lowerBasis, coe_upperClosure, compl_iUnion]
case h.e'_3.h
α : Type u_1
β : Type ?u.6266
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}}
case h.e'_3
α : Type u_1
β : Type ?u.6266
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}}
ext s
case h.e'_3.h.mp
α : Type u_1
β : Type ?u.6266
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}}

case h.e'_3.h.mpr
α : Type u_1
β : Type ?u.6266
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}
case h.e'_3.h
α : Type u_1
β : Type ?u.6266
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}}
constructor
case h.e'_3.h.mp.intro.intro
α : Type u_1
β : Type ?u.6266
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}}
case h.e'_3.h.mp
α : Type u_1
β : Type ?u.6266
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}}
rintro ⟨F, hF, rfl⟩
case h.e'_3.h.mp.intro.intro
α : Type u_1
β : Type ?u.6266
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ᶜ
case h.e'_3.h.mp.intro.intro
α : Type u_1
β : Type ?u.6266
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}}
refine' ⟨(fun a => Ici aᶜ) '' F, ⟨hF.image _, image_subset_iff.2 fun _ _ => ⟨_, rfl⟩⟩, _⟩
no goals
case h.e'_3.h.mp.intro.intro
α : Type u_1
β : Type ?u.6266
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ᶜ
simp only [sInter_image]
case h.e'_3.h.mpr.intro.intro.intro
α : Type u_1
β : Type ?u.6266
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}
case h.e'_3.h.mpr
α : Type u_1
β : Type ?u.6266
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}
rintro ⟨F, ⟨hF, hs⟩, rfl⟩
case h.e'_3.h.mpr.intro.intro.intro
α : Type u_1
β : Type ?u.6266
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}
case h.e'_3.h.mpr.intro.intro.intro
α : Type u_1
β : Type ?u.6266
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}
haveI := hF.to_subtype
case h.e'_3.h.mpr.intro.intro.intro
α : Type u_1
β : Type ?u.6266
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}
case h.e'_3.h.mpr.intro.intro.intro
α : Type u_1
β : Type ?u.6266
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}
rw [subset_def, Subtype.forall'] at hs
case h.e'_3.h.mpr.intro.intro.intro
α : Type u_1
β : Type ?u.6266
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}
case h.e'_3.h.mpr.intro.intro.intro
α : Type u_1
β : Type ?u.6266
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}
choose f hf using hs
no goals
case h.e'_3.h.mpr.intro.intro.intro
α : Type u_1
β : Type ?u.6266
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}
exact ⟨_, finite_range f, by simp_rw [biInter_range, hf, sInter_eq_iInter]⟩
no goals
α : Type u_1
β : Type ?u.6266
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
simp_rw [biInter_range, hf, sInter_eq_iInter]