disjoint_iff — Mathlib

English

For x generic in S and U open, S and U are disjoint iff x ∉ U.

Русский

Для x обобщенной точки S и открытого U верно: Disjoint(S,U) если и только если x ∉ U.

LaTeX

$$$ \mathrm{IsGenericPoint}(x,S) \land \mathrm{IsOpen}(U) \Rightarrow \mathrm{Disjoint}(S,U) \iff x \notin U$$$

Lean4

theorem disjoint_iff (h : IsGenericPoint x S) (hU : IsOpen U) : Disjoint S U ↔ x ∉ U := by
  rw [h.mem_open_set_iff hU, ← not_disjoint_iff_nonempty_inter, Classical.not_not]

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