α : Type u
s : Set (Set α)
⊢ IsTopologicalBasis ((fun f => ⋂₀ f) '' {f | Set.Finite f ∧ f ⊆ s})
α : Type u
t : TopologicalSpace α
s : Set (Set α)
hs : t = generateFrom s
⊢ IsTopologicalBasis ((fun f => ⋂₀ f) '' {f | Set.Finite f ∧ f ⊆ s})
subst t
α : Type u
s : Set (Set α)
this : TopologicalSpace α := generateFrom s
⊢ IsTopologicalBasis ((fun f => ⋂₀ f) '' {f | Set.Finite f ∧ f ⊆ s})
α : Type u
s : Set (Set α)
⊢ IsTopologicalBasis ((fun f => ⋂₀ f) '' {f | Set.Finite f ∧ f ⊆ s})
letI := generateFrom s
case refine'_1
α : Type u
s : Set (Set α)
this : TopologicalSpace α := generateFrom s
⊢ ∀ (t₁ : Set α),
    t₁ ∈ (fun f => ⋂₀ f) '' {f | Set.Finite f ∧ f ⊆ s} →
      ∀ (t₂ : Set α),
        t₂ ∈ (fun f => ⋂₀ f) '' {f | Set.Finite f ∧ f ⊆ s} →
          ∀ (x : α), x ∈ t₁ ∩ t₂ → ∃ t₃, t₃ ∈ (fun f => ⋂₀ f) '' {f | Set.Finite f ∧ f ⊆ s} ∧ x ∈ t₃ ∧ t₃ ⊆ t₁ ∩ t₂

case refine'_2
α : Type u
s : Set (Set α)
this : TopologicalSpace α := generateFrom s
⊢ ⋃₀ ((fun f => ⋂₀ f) '' {f | Set.Finite f ∧ f ⊆ s}) = univ

case refine'_3
α : Type u
s : Set (Set α)
this : TopologicalSpace α := generateFrom s
⊢ ∀ (s_1 : Set α), s_1 ∈ (fun f => ⋂₀ f) '' {f | Set.Finite f ∧ f ⊆ s} → IsOpen s_1

case refine'_4
α : Type u
s : Set (Set α)
this : TopologicalSpace α := generateFrom s
t : Set α
ht : t ∈ s
⊢ t ∈ (fun f => ⋂₀ f) '' {f | Set.Finite f ∧ f ⊆ s}
α : Type u
s : Set (Set α)
this : TopologicalSpace α := generateFrom s
⊢ IsTopologicalBasis ((fun f => ⋂₀ f) '' {f | Set.Finite f ∧ f ⊆ s})
refine' ⟨_, _, le_antisymm (le_generateFrom _) <| generateFrom_anti fun t ht => _⟩
case refine'_1.intro.intro.intro.intro.intro.intro
α : Type u
s : Set (Set α)
this : TopologicalSpace α := generateFrom s
t₁ : Set (Set α)
hft₁ : Set.Finite t₁
ht₁b : t₁ ⊆ s
t₂ : Set (Set α)
hft₂ : Set.Finite t₂
ht₂b : t₂ ⊆ s
x : α
h : x ∈ (fun f => ⋂₀ f) t₁ ∩ (fun f => ⋂₀ f) t₂
⊢ ∃ t₃, t₃ ∈ (fun f => ⋂₀ f) '' {f | Set.Finite f ∧ f ⊆ s} ∧ x ∈ t₃ ∧ t₃ ⊆ (fun f => ⋂₀ f) t₁ ∩ (fun f => ⋂₀ f) t₂
case refine'_1
α : Type u
s : Set (Set α)
this : TopologicalSpace α := generateFrom s
⊢ ∀ (t₁ : Set α),
    t₁ ∈ (fun f => ⋂₀ f) '' {f | Set.Finite f ∧ f ⊆ s} →
      ∀ (t₂ : Set α),
        t₂ ∈ (fun f => ⋂₀ f) '' {f | Set.Finite f ∧ f ⊆ s} →
          ∀ (x : α), x ∈ t₁ ∩ t₂ → ∃ t₃, t₃ ∈ (fun f => ⋂₀ f) '' {f | Set.Finite f ∧ f ⊆ s} ∧ x ∈ t₃ ∧ t₃ ⊆ t₁ ∩ t₂
rintro _ ⟨t₁, ⟨hft₁, ht₁b⟩, rfl⟩ _ ⟨t₂, ⟨hft₂, ht₂b⟩, rfl⟩ x h
no goals
case refine'_1.intro.intro.intro.intro.intro.intro
α : Type u
s : Set (Set α)
this : TopologicalSpace α := generateFrom s
t₁ : Set (Set α)
hft₁ : Set.Finite t₁
ht₁b : t₁ ⊆ s
t₂ : Set (Set α)
hft₂ : Set.Finite t₂
ht₂b : t₂ ⊆ s
x : α
h : x ∈ (fun f => ⋂₀ f) t₁ ∩ (fun f => ⋂₀ f) t₂
⊢ ∃ t₃, t₃ ∈ (fun f => ⋂₀ f) '' {f | Set.Finite f ∧ f ⊆ s} ∧ x ∈ t₃ ∧ t₃ ⊆ (fun f => ⋂₀ f) t₁ ∩ (fun f => ⋂₀ f) t₂
exact ⟨_, ⟨_, ⟨hft₁.union hft₂, union_subset ht₁b ht₂b⟩, sInter_union t₁ t₂⟩, h, Subset.rfl⟩
case refine'_2
α : Type u
s : Set (Set α)
this : TopologicalSpace α := generateFrom s
⊢ ∀ (a : α), ∃ i j, a ∈ ⋂₀ i
case refine'_2
α : Type u
s : Set (Set α)
this : TopologicalSpace α := generateFrom s
⊢ ⋃₀ ((fun f => ⋂₀ f) '' {f | Set.Finite f ∧ f ⊆ s}) = univ
rw [sUnion_image, iUnion₂_eq_univ_iff]
no goals
case refine'_2
α : Type u
s : Set (Set α)
this : TopologicalSpace α := generateFrom s
⊢ ∀ (a : α), ∃ i j, a ∈ ⋂₀ i
exact fun x => ⟨∅, ⟨finite_empty, empty_subset _⟩, sInter_empty.substr <| mem_univ x⟩
case refine'_3.intro.intro.intro
α : Type u
s : Set (Set α)
this : TopologicalSpace α := generateFrom s
t : Set (Set α)
hft : Set.Finite t
htb : t ⊆ s
⊢ IsOpen ((fun f => ⋂₀ f) t)
case refine'_3
α : Type u
s : Set (Set α)
this : TopologicalSpace α := generateFrom s
⊢ ∀ (s_1 : Set α), s_1 ∈ (fun f => ⋂₀ f) '' {f | Set.Finite f ∧ f ⊆ s} → IsOpen s_1
rintro _ ⟨t, ⟨hft, htb⟩, rfl⟩
case refine'_3.intro.intro.intro.hs
α : Type u
s : Set (Set α)
this : TopologicalSpace α := generateFrom s
t : Set (Set α)
hft : Set.Finite t
htb : t ⊆ s
⊢ Set.Finite t

case refine'_3.intro.intro.intro.a
α : Type u
s : Set (Set α)
this : TopologicalSpace α := generateFrom s
t : Set (Set α)
hft : Set.Finite t
htb : t ⊆ s
⊢ ∀ (t_1 : Set α), t_1 ∈ t → IsOpen t_1
case refine'_3.intro.intro.intro
α : Type u
s : Set (Set α)
this : TopologicalSpace α := generateFrom s
t : Set (Set α)
hft : Set.Finite t
htb : t ⊆ s
⊢ IsOpen ((fun f => ⋂₀ f) t)
apply isOpen_sInter
no goals
case refine'_3.intro.intro.intro.hs
α : Type u
s : Set (Set α)
this : TopologicalSpace α := generateFrom s
t : Set (Set α)
hft : Set.Finite t
htb : t ⊆ s
⊢ Set.Finite t

case refine'_3.intro.intro.intro.a
α : Type u
s : Set (Set α)
this : TopologicalSpace α := generateFrom s
t : Set (Set α)
hft : Set.Finite t
htb : t ⊆ s
⊢ ∀ (t_1 : Set α), t_1 ∈ t → IsOpen t_1
exacts [hft, fun s hs => GenerateOpen.basic _ <| htb hs]
case refine'_4
α : Type u
s : Set (Set α)
this : TopologicalSpace α := generateFrom s
t : Set α
ht : t ∈ s
⊢ ⋂₀ {t} ∈ (fun f => ⋂₀ f) '' {f | Set.Finite f ∧ f ⊆ s}
case refine'_4
α : Type u
s : Set (Set α)
this : TopologicalSpace α := generateFrom s
t : Set α
ht : t ∈ s
⊢ t ∈ (fun f => ⋂₀ f) '' {f | Set.Finite f ∧ f ⊆ s}
rw [← sInter_singleton t]
no goals
case refine'_4
α : Type u
s : Set (Set α)
this : TopologicalSpace α := generateFrom s
t : Set α
ht : t ∈ s
⊢ ⋂₀ {t} ∈ (fun f => ⋂₀ f) '' {f | Set.Finite f ∧ f ⊆ s}
exact ⟨{t}, ⟨finite_singleton t, singleton_subset_iff.2 ht⟩, rfl⟩