disjoint_nhds_atBot_iff — Mathlib

English

In a topological preorder with ClosedIicTopology, for any a, Disjoint(nhds a, atBot) holds exactly when a is not the bottom element.

Русский

В топологическом порядке с ClosedIicTopology выполняется: Disjoint(nhds(a), atBot) тогда и только тогда, когда a не минимальный элемент.

LaTeX

$$Disjoint(nhds(a), atBot) \iff \neg IsBot(a)$$

Lean4

@[simp]
theorem disjoint_nhds_atBot_iff : Disjoint (𝓝 a) atBot ↔ ¬IsBot a :=
  by
  constructor
  · intro hd hbot
    rw [hbot.atBot_eq, disjoint_principal_right] at hd
    exact mem_of_mem_nhds hd le_rfl
  · simp only [IsBot, not_forall]
    rintro ⟨b, hb⟩
    refine disjoint_of_disjoint_of_mem disjoint_compl_left ?_ (Iic_mem_atBot b)
    exact isClosed_Iic.isOpen_compl.mem_nhds hb

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