[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
X : Type u_4
Y : Type u_5
s : Set α
⊢ IsOpen {l | s ∈ l}
[PROOFSTEP]
simpa only [Iic_principal] using isOpen_Iic_principal
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
X : Type u_4
Y : Type u_5
⊢ ∀ (t₁ : Set (Filter α)),
    t₁ ∈ range (Iic ∘ 𝓟) →
      ∀ (t₂ : Set (Filter α)),
        t₂ ∈ range (Iic ∘ 𝓟) → ∀ (x : Filter α), x ∈ t₁ ∩ t₂ → ∃ t₃, t₃ ∈ range (Iic ∘ 𝓟) ∧ x ∈ t₃ ∧ t₃ ⊆ t₁ ∩ t₂
[PROOFSTEP]
rintro _ ⟨s, rfl⟩ _ ⟨t, rfl⟩ l hl
[GOAL]
case intro.intro
ι : Sort u_1
α : Type u_2
β : Type u_3
X : Type u_4
Y : Type u_5
s t : Set α
l : Filter α
hl : l ∈ (Iic ∘ 𝓟) s ∩ (Iic ∘ 𝓟) t
⊢ ∃ t₃, t₃ ∈ range (Iic ∘ 𝓟) ∧ l ∈ t₃ ∧ t₃ ⊆ (Iic ∘ 𝓟) s ∩ (Iic ∘ 𝓟) t
[PROOFSTEP]
exact ⟨Iic (𝓟 s) ∩ Iic (𝓟 t), ⟨s ∩ t, by simp⟩, hl, Subset.rfl⟩
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
X : Type u_4
Y : Type u_5
s t : Set α
l : Filter α
hl : l ∈ (Iic ∘ 𝓟) s ∩ (Iic ∘ 𝓟) t
⊢ (Iic ∘ 𝓟) (s ∩ t) = Iic (𝓟 s) ∩ Iic (𝓟 t)
[PROOFSTEP]
simp
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
X : Type u_4
Y : Type u_5
s : Set (Filter α)
⊢ (∃ S, S ⊆ range (Iic ∘ 𝓟) ∧ s = ⋃₀ S) ↔ ∃ T, s = ⋃ (t : Set α) (_ : t ∈ T), Iic (𝓟 t)
[PROOFSTEP]
simp only [exists_subset_range_and_iff, sUnion_image, (· ∘ ·)]
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
X : Type u_4
Y : Type u_5
l : Filter α
⊢ ⨅ (s : Set (Filter α)) (_ : s ∈ {s | l ∈ s ∧ s ∈ range (Iic ∘ 𝓟)}), 𝓟 s = Filter.lift' l (Iic ∘ 𝓟)
[PROOFSTEP]
simp only [mem_setOf_eq, @and_comm (l ∈ _), iInf_and, iInf_range, Filter.lift', Filter.lift, (· ∘ ·), mem_Iic,
  le_principal_iff]
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
X : Type u_4
Y : Type u_5
l : Filter α
⊢ 𝓝 l = Filter.lift' l fun s => {l' | s ∈ l'}
[PROOFSTEP]
simpa only [(· ∘ ·), Iic_principal] using nhds_eq l
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
X : Type u_4
Y : Type u_5
la : Filter α
lb : Filter β
f : α → Filter β
⊢ Tendsto f la (𝓝 lb) ↔ ∀ (s : Set β), s ∈ lb → ∀ᶠ (a : α) in la, s ∈ f a
[PROOFSTEP]
simp only [nhds_eq', tendsto_lift', mem_setOf_eq]
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
X : Type u_4
Y : Type u_5
l : Filter α
p : ι → Prop
s : ι → Set α
h : HasBasis l p s
⊢ HasBasis (𝓝 l) p fun i => Iic (𝓟 (s i))
[PROOFSTEP]
rw [nhds_eq]
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
X : Type u_4
Y : Type u_5
l : Filter α
p : ι → Prop
s : ι → Set α
h : HasBasis l p s
⊢ HasBasis (Filter.lift' l (Iic ∘ 𝓟)) p fun i => Iic (𝓟 (s i))
[PROOFSTEP]
exact h.lift' monotone_principal.Iic
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
X : Type u_4
Y : Type u_5
l : Filter X
⊢ Tendsto pure l (𝓝 l)
[PROOFSTEP]
rw [Filter.tendsto_nhds]
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
X : Type u_4
Y : Type u_5
l : Filter X
⊢ ∀ (s : Set X), s ∈ l → ∀ᶠ (a : X) in l, s ∈ pure a
[PROOFSTEP]
refine fun s hs ↦ Eventually.mono hs fun x ↦ id
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
X : Type u_4
Y : Type u_5
l : Filter α
p : ι → Prop
s : ι → Set α
h : HasBasis l p s
⊢ HasBasis (𝓝 l) p fun i => {l' | s i ∈ l'}
[PROOFSTEP]
simpa only [Iic_principal] using h.nhds
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
X : Type u_4
Y : Type u_5
⊢ 𝓝 ⊥ = pure ⊥
[PROOFSTEP]
simp [nhds_eq, (· ∘ ·), lift'_bot monotone_principal.Iic]
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
X : Type u_4
Y : Type u_5
⊢ 𝓝 ⊤ = ⊤
[PROOFSTEP]
simp [nhds_eq]
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
X : Type u_4
Y : Type u_5
x : α
⊢ 𝓝 (pure x) = 𝓟 {⊥, pure x}
[PROOFSTEP]
rw [← principal_singleton, nhds_principal, principal_singleton, Iic_pure]
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
X : Type u_4
Y : Type u_5
f : ι → Filter α
⊢ 𝓝 (⨅ (i : ι), f i) = ⨅ (i : ι), 𝓝 (f i)
[PROOFSTEP]
simp only [nhds_eq]
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
X : Type u_4
Y : Type u_5
f : ι → Filter α
⊢ Filter.lift' (⨅ (i : ι), f i) (Iic ∘ 𝓟) = ⨅ (i : ι), Filter.lift' (f i) (Iic ∘ 𝓟)
[PROOFSTEP]
apply lift'_iInf_of_map_univ
[GOAL]
case hg
ι : Sort u_1
α : Type u_2
β : Type u_3
X : Type u_4
Y : Type u_5
f : ι → Filter α
⊢ ∀ {s t : Set α}, (Iic ∘ 𝓟) (s ∩ t) = (Iic ∘ 𝓟) s ∩ (Iic ∘ 𝓟) t
[PROOFSTEP]
simp
[GOAL]
case hg'
ι : Sort u_1
α : Type u_2
β : Type u_3
X : Type u_4
Y : Type u_5
f : ι → Filter α
⊢ (Iic ∘ 𝓟) univ = univ
[PROOFSTEP]
simp
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
X : Type u_4
Y : Type u_5
l₁ l₂ : Filter α
⊢ 𝓝 (l₁ ⊓ l₂) = 𝓝 l₁ ⊓ 𝓝 l₂
[PROOFSTEP]
simpa only [iInf_bool_eq] using nhds_iInf fun b => cond b l₁ l₂
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
X : Type u_4
Y : Type u_5
l : Filter α
⊢ ⋂₀ {s | s ∈ 𝓝 l} = Iic l
[PROOFSTEP]
simp_rw [nhds_eq, (· ∘ ·), sInter_lift'_sets monotone_principal.Iic, Iic, le_principal_iff, ← setOf_forall, ←
  Filter.le_def]
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
X : Type u_4
Y : Type u_5
l₁ l₂ : Filter α
⊢ 𝓝 l₁ ≤ 𝓝 l₂ ↔ l₁ ≤ l₂
[PROOFSTEP]
refine' ⟨fun h => _, fun h => monotone_nhds h⟩
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
X : Type u_4
Y : Type u_5
l₁ l₂ : Filter α
h : 𝓝 l₁ ≤ 𝓝 l₂
⊢ l₁ ≤ l₂
[PROOFSTEP]
rw [← Iic_subset_Iic, ← sInter_nhds, ← sInter_nhds]
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
X : Type u_4
Y : Type u_5
l₁ l₂ : Filter α
h : 𝓝 l₁ ≤ 𝓝 l₂
⊢ ⋂₀ {s | s ∈ 𝓝 l₁} ⊆ ⋂₀ {s | s ∈ 𝓝 l₂}
[PROOFSTEP]
exact sInter_subset_sInter h
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
X : Type u_4
Y : Type u_5
s : Set (Filter α)
l : Filter α
⊢ l ∈ interior s ↔ ∃ t, t ∈ l ∧ Iic (𝓟 t) ⊆ s
[PROOFSTEP]
rw [mem_interior_iff_mem_nhds, mem_nhds_iff]
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
X : Type u_4
Y : Type u_5
s : Set (Filter α)
l : Filter α
⊢ l ∈ closure s ↔ ∀ (t : Set α), t ∈ l → ∃ l', l' ∈ s ∧ t ∈ l'
[PROOFSTEP]
simp only [closure_eq_compl_interior_compl, Filter.mem_interior, mem_compl_iff, not_exists, not_forall,
  Classical.not_not, exists_prop, not_and, and_comm, subset_def, mem_Iic, le_principal_iff]
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
X : Type u_4
Y : Type u_5
l : Filter α
⊢ closure {l} = Ici l
[PROOFSTEP]
ext l'
[GOAL]
case h
ι : Sort u_1
α : Type u_2
β : Type u_3
X : Type u_4
Y : Type u_5
l l' : Filter α
⊢ l' ∈ closure {l} ↔ l' ∈ Ici l
[PROOFSTEP]
simp [Filter.mem_closure, Filter.le_def]
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
X : Type u_4
Y : Type u_5
l₁ l₂ : Filter α
⊢ l₁ ⤳ l₂ ↔ l₁ ≤ l₂
[PROOFSTEP]
simp only [specializes_iff_closure_subset, Filter.closure_singleton, Ici_subset_Ici]
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
X : Type u_4
Y : Type u_5
inst✝ : Preorder α
⊢ 𝓝 atTop = ⨅ (x : α), 𝓟 (Iic (𝓟 (Ici x)))
[PROOFSTEP]
simp only [atTop, nhds_iInf, nhds_principal]
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
X : Type u_4
Y : Type u_5
inst✝ : Preorder β
l : Filter α
f : α → Filter β
⊢ Tendsto f l (𝓝 atTop) ↔ ∀ (y : β), ∀ᶠ (a : α) in l, Ici y ∈ f a
[PROOFSTEP]
simp only [nhds_atTop, tendsto_iInf, tendsto_principal, mem_Iic, le_principal_iff]
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
X : Type u_4
Y : Type u_5
inst✝ : TopologicalSpace X
x : X
⊢ 𝓝 (𝓝 x) = ⨅ (s : Set X) (_ : IsOpen s) (_ : x ∈ s), 𝓟 (Iic (𝓟 s))
[PROOFSTEP]
simp only [(nhds_basis_opens x).nhds.eq_biInf, iInf_and, @iInf_comm _ (_ ∈ _)]
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
X : Type u_4
Y : Type u_5
inst✝ : TopologicalSpace X
x : X
⊢ ⨅ (s : Set X) (_ : IsOpen s) (_ : x ∈ s), 𝓟 s = comap 𝓝 (𝓝 (𝓝 x))
[PROOFSTEP]
simp (config := { contextual := true }) only [nhds_nhds, comap_iInf, comap_principal, Iic_principal, preimage_setOf_eq,
  ← mem_interior_iff_mem_nhds, setOf_mem_eq, IsOpen.interior_eq]
