α : Type u
b : Ultrafilter α
⊢ comap pure (⨅ (s : Set (Ultrafilter α)) (_ : s ∈ {s | b ∈ s ∧ s ∈ ultrafilterBasis α}), 𝓟 s) ≤ ↑b
α : Type u
b : Ultrafilter α
⊢ comap pure (𝓝 b) ≤ ↑b
rw [TopologicalSpace.nhds_generateFrom]
α : Type u
b : Ultrafilter α
⊢ (⨅ (i : Set (Ultrafilter α)) (_ : i ∈ {s | b ∈ s ∧ s ∈ ultrafilterBasis α}), 𝓟 (pure ⁻¹' i)) ≤ ↑b
α : Type u
b : Ultrafilter α
⊢ comap pure (⨅ (s : Set (Ultrafilter α)) (_ : s ∈ {s | b ∈ s ∧ s ∈ ultrafilterBasis α}), 𝓟 s) ≤ ↑b
simp only [comap_iInf, comap_principal]
α : Type u
b : Ultrafilter α
s : Set α
hs : s ∈ ↑b
⊢ s ∈ ⨅ (i : Set (Ultrafilter α)) (_ : i ∈ {s | b ∈ s ∧ s ∈ ultrafilterBasis α}), 𝓟 (pure ⁻¹' i)
α : Type u
b : Ultrafilter α
⊢ (⨅ (i : Set (Ultrafilter α)) (_ : i ∈ {s | b ∈ s ∧ s ∈ ultrafilterBasis α}), 𝓟 (pure ⁻¹' i)) ≤ ↑b
intro s hs
α : Type u
b : Ultrafilter α
s : Set α
hs : s ∈ ↑b
⊢ (⨅ (i : Set (Ultrafilter α)) (_ : i ∈ {s | b ∈ s ∧ s ∈ ultrafilterBasis α}), 𝓟 (pure ⁻¹' i)) ≤ 𝓟 s
α : Type u
b : Ultrafilter α
s : Set α
hs : s ∈ ↑b
⊢ s ∈ ⨅ (i : Set (Ultrafilter α)) (_ : i ∈ {s | b ∈ s ∧ s ∈ ultrafilterBasis α}), 𝓟 (pure ⁻¹' i)
rw [← le_principal_iff]
α : Type u
b : Ultrafilter α
s : Set α
hs : s ∈ ↑b
⊢ (⨅ (_ : {u | s ∈ u} ∈ {s | b ∈ s ∧ s ∈ ultrafilterBasis α}), 𝓟 (pure ⁻¹' {u | s ∈ u})) ≤ 𝓟 s
α : Type u
b : Ultrafilter α
s : Set α
hs : s ∈ ↑b
⊢ (⨅ (i : Set (Ultrafilter α)) (_ : i ∈ {s | b ∈ s ∧ s ∈ ultrafilterBasis α}), 𝓟 (pure ⁻¹' i)) ≤ 𝓟 s
refine' iInf_le_of_le { u | s ∈ u } _
α : Type u
b : Ultrafilter α
s : Set α
hs : s ∈ ↑b
⊢ 𝓟 (pure ⁻¹' {u | s ∈ u}) ≤ 𝓟 s
α : Type u
b : Ultrafilter α
s : Set α
hs : s ∈ ↑b
⊢ (⨅ (_ : {u | s ∈ u} ∈ {s | b ∈ s ∧ s ∈ ultrafilterBasis α}), 𝓟 (pure ⁻¹' {u | s ∈ u})) ≤ 𝓟 s
refine' iInf_le_of_le ⟨hs, ⟨s, rfl⟩⟩ _
no goals
α : Type u
b : Ultrafilter α
s : Set α
hs : s ∈ ↑b
⊢ 𝓟 (pure ⁻¹' {u | s ∈ u}) ≤ 𝓟 s
exact principal_mono.2 fun a => id