le_iff_nhds — Mathlib

English

A relation t ≤ t' between topologies is equivalent to pointwise inclusion of neighborhood filters.

Русский

Отношение t ≤ t' между топологиями эквивалентно вложению фильтров окрестностей в каждой точке.

LaTeX

$$$t \le t' \iff \forall x, @nhds α t x \le @nhds α t' x$$

Lean4

theorem le_iff_nhds {α : Type*} (t t' : TopologicalSpace α) : t ≤ t' ↔ ∀ x, @nhds α t x ≤ @nhds α t' x :=
  ⟨fun h _ => nhds_mono h, le_of_nhds_le_nhds⟩

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