Theorems · Theorem · general topology

le_nhds_lim

∀ {X : Type u} [inst : TopologicalSpace X] {f : Filter X} (h : ∃ x, f ≤ nhds x), f ≤ nhds f.lim

If a filter f is majorated by some 𝓝 x, then it is majorated by 𝓝 (Filter.lim f). We formulate this lemma with a [Nonempty X] argument of lim derived from h to make it useful for types without a [Nonempty X] instance. Because of the built-in proof irrelevance, Lean will unify this instance with any other instance.

Defined in

Mathlib.Topology.Basic

Cited by

5 results in Mathlib

Foundations

Depth 20 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpace