isOpen_iff_forall_specializes — Mathlib

English

A set is open precisely when it contains every specialization chain from x to y whenever x specializes to y and y lies in the set.

Русский

Множество открыто тогда, когда содержит каждую цепь специализации от x до y, если x специализируется на y и y принадлежит множеству.

LaTeX

$$IsOpen s ↔ ∀ x y, x ⤳ y → y ∈ s → x ∈ s$$

Lean4

theorem isOpen_iff_forall_specializes : IsOpen s ↔ ∀ x y, x ⤳ y → y ∈ s → x ∈ s := by
  simp only [← nhdsKer_subset_iff_isOpen, Set.subset_def, mem_nhdsKer_iff_specializes, exists_imp, and_imp,
    @forall_swap (_ ⤳ _)]

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