case refine'_1
α : Type u
t : TopologicalSpace α
s : Set (Set α)
h_open : ∀ (u : Set α), u ∈ s → IsOpen u
h_nhds : ∀ (a : α) (u : Set α), a ∈ u → IsOpen u → ∃ v, v ∈ s ∧ a ∈ v ∧ v ⊆ u
⊢ ⋃₀ s = univ

case refine'_2
α : Type u
t : TopologicalSpace α
s : Set (Set α)
h_open : ∀ (u : Set α), u ∈ s → IsOpen u
h_nhds : ∀ (a : α) (u : Set α), a ∈ u → IsOpen u → ∃ v, v ∈ s ∧ a ∈ v ∧ v ⊆ u
⊢ t = generateFrom s
α : Type u
t : TopologicalSpace α
s : Set (Set α)
h_open : ∀ (u : Set α), u ∈ s → IsOpen u
h_nhds : ∀ (a : α) (u : Set α), a ∈ u → IsOpen u → ∃ v, v ∈ s ∧ a ∈ v ∧ v ⊆ u
⊢ IsTopologicalBasis s
refine'
  ⟨fun t₁ ht₁ t₂ ht₂ x hx => h_nhds _ _ hx (IsOpen.inter (h_open _ ht₁) (h_open _ ht₂)), _, _⟩
case refine'_1
α : Type u
t : TopologicalSpace α
s : Set (Set α)
h_open : ∀ (u : Set α), u ∈ s → IsOpen u
h_nhds : ∀ (a : α) (u : Set α), a ∈ u → IsOpen u → ∃ v, v ∈ s ∧ a ∈ v ∧ v ⊆ u
a : α
⊢ ∃ b, b ∈ s ∧ a ∈ b
case refine'_1
α : Type u
t : TopologicalSpace α
s : Set (Set α)
h_open : ∀ (u : Set α), u ∈ s → IsOpen u
h_nhds : ∀ (a : α) (u : Set α), a ∈ u → IsOpen u → ∃ v, v ∈ s ∧ a ∈ v ∧ v ⊆ u
⊢ ⋃₀ s = univ
refine' sUnion_eq_univ_iff.2 fun a => _
case refine'_1.intro.intro.intro
α : Type u
t : TopologicalSpace α
s : Set (Set α)
h_open : ∀ (u : Set α), u ∈ s → IsOpen u
h_nhds : ∀ (a : α) (u : Set α), a ∈ u → IsOpen u → ∃ v, v ∈ s ∧ a ∈ v ∧ v ⊆ u
a : α
u : Set α
h₁ : u ∈ s
h₂ : a ∈ u
⊢ ∃ b, b ∈ s ∧ a ∈ b
case refine'_1
α : Type u
t : TopologicalSpace α
s : Set (Set α)
h_open : ∀ (u : Set α), u ∈ s → IsOpen u
h_nhds : ∀ (a : α) (u : Set α), a ∈ u → IsOpen u → ∃ v, v ∈ s ∧ a ∈ v ∧ v ⊆ u
a : α
⊢ ∃ b, b ∈ s ∧ a ∈ b
rcases h_nhds a univ trivial isOpen_univ with ⟨u, h₁, h₂, -⟩
no goals
case refine'_1.intro.intro.intro
α : Type u
t : TopologicalSpace α
s : Set (Set α)
h_open : ∀ (u : Set α), u ∈ s → IsOpen u
h_nhds : ∀ (a : α) (u : Set α), a ∈ u → IsOpen u → ∃ v, v ∈ s ∧ a ∈ v ∧ v ⊆ u
a : α
u : Set α
h₁ : u ∈ s
h₂ : a ∈ u
⊢ ∃ b, b ∈ s ∧ a ∈ b
exact ⟨u, h₁, h₂⟩
case refine'_2
α : Type u
t : TopologicalSpace α
s : Set (Set α)
h_open : ∀ (u : Set α), u ∈ s → IsOpen u
h_nhds : ∀ (a : α) (u : Set α), a ∈ u → IsOpen u → ∃ v, v ∈ s ∧ a ∈ v ∧ v ⊆ u
u : Set α
hu : IsOpen u
⊢ IsOpen u
case refine'_2
α : Type u
t : TopologicalSpace α
s : Set (Set α)
h_open : ∀ (u : Set α), u ∈ s → IsOpen u
h_nhds : ∀ (a : α) (u : Set α), a ∈ u → IsOpen u → ∃ v, v ∈ s ∧ a ∈ v ∧ v ⊆ u
⊢ t = generateFrom s
refine' (le_generateFrom h_open).antisymm fun u hu => _
case refine'_2
α : Type u
t : TopologicalSpace α
s : Set (Set α)
h_open : ∀ (u : Set α), u ∈ s → IsOpen u
h_nhds : ∀ (a : α) (u : Set α), a ∈ u → IsOpen u → ∃ v, v ∈ s ∧ a ∈ v ∧ v ⊆ u
u : Set α
hu : IsOpen u
a : α
ha : a ∈ u
⊢ 𝓝 a ≤ 𝓟 u
case refine'_2
α : Type u
t : TopologicalSpace α
s : Set (Set α)
h_open : ∀ (u : Set α), u ∈ s → IsOpen u
h_nhds : ∀ (a : α) (u : Set α), a ∈ u → IsOpen u → ∃ v, v ∈ s ∧ a ∈ v ∧ v ⊆ u
u : Set α
hu : IsOpen u
⊢ IsOpen u
refine' (@isOpen_iff_nhds α (generateFrom s) u).mpr fun a ha => _
case refine'_2.intro.intro.intro
α : Type u
t : TopologicalSpace α
s : Set (Set α)
h_open : ∀ (u : Set α), u ∈ s → IsOpen u
h_nhds : ∀ (a : α) (u : Set α), a ∈ u → IsOpen u → ∃ v, v ∈ s ∧ a ∈ v ∧ v ⊆ u
u : Set α
hu : IsOpen u
a : α
ha : a ∈ u
v : Set α
hvs : v ∈ s
hav : a ∈ v
hvu : v ⊆ u
⊢ 𝓝 a ≤ 𝓟 u
case refine'_2
α : Type u
t : TopologicalSpace α
s : Set (Set α)
h_open : ∀ (u : Set α), u ∈ s → IsOpen u
h_nhds : ∀ (a : α) (u : Set α), a ∈ u → IsOpen u → ∃ v, v ∈ s ∧ a ∈ v ∧ v ⊆ u
u : Set α
hu : IsOpen u
a : α
ha : a ∈ u
⊢ 𝓝 a ≤ 𝓟 u
rcases h_nhds a u ha hu with ⟨v, hvs, hav, hvu⟩
case refine'_2.intro.intro.intro
α : Type u
t : TopologicalSpace α
s : Set (Set α)
h_open : ∀ (u : Set α), u ∈ s → IsOpen u
h_nhds : ∀ (a : α) (u : Set α), a ∈ u → IsOpen u → ∃ v, v ∈ s ∧ a ∈ v ∧ v ⊆ u
u : Set α
hu : IsOpen u
a : α
ha : a ∈ u
v : Set α
hvs : v ∈ s
hav : a ∈ v
hvu : v ⊆ u
⊢ (⨅ (s_1 : Set α) (_ : s_1 ∈ {s_2 | a ∈ s_2 ∧ s_2 ∈ s}), 𝓟 s_1) ≤ 𝓟 u
case refine'_2.intro.intro.intro
α : Type u
t : TopologicalSpace α
s : Set (Set α)
h_open : ∀ (u : Set α), u ∈ s → IsOpen u
h_nhds : ∀ (a : α) (u : Set α), a ∈ u → IsOpen u → ∃ v, v ∈ s ∧ a ∈ v ∧ v ⊆ u
u : Set α
hu : IsOpen u
a : α
ha : a ∈ u
v : Set α
hvs : v ∈ s
hav : a ∈ v
hvu : v ⊆ u
⊢ 𝓝 a ≤ 𝓟 u
rw [nhds_generateFrom]
no goals
case refine'_2.intro.intro.intro
α : Type u
t : TopologicalSpace α
s : Set (Set α)
h_open : ∀ (u : Set α), u ∈ s → IsOpen u
h_nhds : ∀ (a : α) (u : Set α), a ∈ u → IsOpen u → ∃ v, v ∈ s ∧ a ∈ v ∧ v ⊆ u
u : Set α
hu : IsOpen u
a : α
ha : a ∈ u
v : Set α
hvs : v ∈ s
hav : a ∈ v
hvu : v ⊆ u
⊢ (⨅ (s_1 : Set α) (_ : s_1 ∈ {s_2 | a ∈ s_2 ∧ s_2 ∈ s}), 𝓟 s_1) ≤ 𝓟 u
exact iInf₂_le_of_le v ⟨hav, hvs⟩ (le_principal_iff.2 hvu)