isGenericPoint_iff_specializes — Mathlib

English

There is a characterization: IsGenericPoint x S holds exactly when every specialization from x to y corresponds to y ∈ S; i.e., IsGenericPoint x S ⇔ ∀ y, x ⤳ y ⇔ y ∈ S.

Русский

Характеризация: IsGenericPoint x S реализуется тогда и только тогда, когда для всех y выполняется x ⤳ y ⇔ y ∈ S.

LaTeX

$$$ \mathrm{IsGenericPoint}(x,S) \iff \forall y\, (x \rightsquigarrow y) \iff y \in S$$$

Lean4

theorem isGenericPoint_iff_specializes : IsGenericPoint x S ↔ ∀ y, x ⤳ y ↔ y ∈ S := by
  simp only [specializes_iff_mem_closure, IsGenericPoint, Set.ext_iff]

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