mem_nhdsKer_iff_specializes — Mathlib

English

x ∈ nhdsKer(s) iff ∃ y ∈ s with x specializes to y.

Русский

x ∈ nhdsKer(s) тогда и только тогда, когда существует y ∈ s, для которого x специализируется на y.

LaTeX

$$x ∈ nhdsKer(s) ↔ ∃ y ∈ s, x ⤳ y$$

Lean4

theorem mem_nhdsKer_iff_specializes : x ∈ nhdsKer s ↔ ∃ y ∈ s, x ⤳ y :=
  calc
    x ∈ nhdsKer s ↔ x ∈ nhdsKer (⋃ y ∈ s, { y }) := by simp
    _ ↔ ∃ y ∈ s, x ⤳ y := by simp only [nhdsKer_iUnion, mem_nhdsKer_singleton, mem_iUnion₂, exists_prop]

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