isOpen — Mathlib

English

For any Realizer F and any index, the corresponding realized set is open.

Русский

Для любого реализатора F и индекса соответствующее реализованное множество открыто.

LaTeX

$$$\\text{Realizer.isOpen}(F, s) : IsOpen(F.F s)$$$

Lean4

protected theorem isOpen [TopologicalSpace α] (F : Realizer α) (s : F.σ) : IsOpen (F.F s) :=
  isOpen_iff_nhds.2 fun a m ↦ by simpa using F.mem_nhds.2 ⟨s, m, Subset.refl _⟩

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