le_of_nhds_le_nhds — Mathlib

English

If nhds^t1(x) ≤ nhds^t2(x) for all x, then the topology t1 is less than or equal to t2 (t1 ≤ t2).

Русский

Если окрестностный фильтр в t1 меньше или равен окрестностному фильтру в t2 для каждой точки x, то топология t1 не более чем t2.

LaTeX

$$$(\forall x,\ nhds_{t_1}(x) \le nhds_{t_2}(x)) \Rightarrow t_1 \le t_2$$$

Lean4

theorem le_of_nhds_le_nhds (h : ∀ x, @nhds α t₁ x ≤ @nhds α t₂ x) : t₁ ≤ t₂ := fun s =>
  by
  rw [@isOpen_iff_mem_nhds _ t₁, @isOpen_iff_mem_nhds _ t₂]
  exact fun hs a ha => h _ (hs _ ha)

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