mem_open_set_iff — Mathlib

English

If x is generic point of S and U is open, then x ∈ U iff (S ∩ U) is nonempty.

Русский

Если x обобщенная точка S и U открыто, то x ∈ U тогда и только тогда, когда S ∩ U непусто.

LaTeX

$$$ \mathrm{IsGenericPoint}(x,S) \land \mathrm{IsOpen}(U) \Rightarrow (x \in U) \iff (S \cap U) \neq \emptyset$$$

Lean4

theorem mem_open_set_iff (h : IsGenericPoint x S) (hU : IsOpen U) : x ∈ U ↔ (S ∩ U).Nonempty :=
  ⟨fun h' => ⟨x, h.mem, h'⟩, fun ⟨_y, hyS, hyU⟩ => (h.specializes hyS).mem_open hU hyU⟩

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