isOpen_iff — Mathlib

English

An open set in the topology realized by F is characterized by realizations witnessing its openness.

Русский

Открытое множество в топологии, реализованной F, характеризуется реализациями, доказывающими открытость.

LaTeX

$$$IsOpen(s) \\iff \\forall a\\in s, \\exists b, a\\in F.F b ∧ F.F b ⊆ s$$$

Lean4

theorem isOpen_iff [TopologicalSpace α] (F : Realizer α) {s : Set α} : IsOpen s ↔ ∀ a ∈ s, ∃ b, a ∈ F.F b ∧ F.F b ⊆ s :=
  isOpen_iff_mem_nhds.trans <| forall₂_congr fun _a _h ↦ F.mem_nhds

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