isClosed_setOf_specializes — Mathlib

English

The set of all pairs (x,y) in X×X such that x specializes to y is a closed subset of X×X.

Русский

Множество всех упорядоченных пар (x,y) в X×X, для которых x специализируется на y, замкнуто в X×X.

LaTeX

$$$ IsClosed \\{p : X \\times X \\mid p.1 \\triangleright p.2\\}. $$$

Lean4

theorem isClosed_setOf_specializes : IsClosed {p : X × X | p.1 ⤳ p.2} := by
  simp only [← isOpen_compl_iff, compl_setOf, ← disjoint_nhds_nhds_iff_not_specializes, isOpen_setOf_disjoint_nhds_nhds]

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