ultrafilter_comap_pure_nhds — Mathlib

English

For every ultrafilter b on α, the comap of nhds(b) along pure is contained in b: comap pure (𝓝 b) ≤ b.

Русский

Для каждого ультрафильтра b на α выполняется comap pure (𝓝 b) ≤ b.

LaTeX

$$$\operatorname{comap}\;\mathrm{pure}\ (𝓝 b) \le b$$$

Lean4

theorem ultrafilter_comap_pure_nhds (b : Ultrafilter α) : comap pure (𝓝 b) ≤ b :=
  by
  rw [TopologicalSpace.nhds_generateFrom]
  simp only [comap_iInf, comap_principal]
  intro s hs
  rw [← le_principal_iff]
  refine iInf_le_of_le {u | s ∈ u} ?_
  refine iInf_le_of_le ⟨hs, ⟨s, rfl⟩⟩ ?_
  exact principal_mono.2 fun _ ↦ id

Похожие утверждения