Union_closure_singleton_eq_iff — Mathlib

English

The union over x in s of closures of {x} equals s if and only if s is stable under specialization.

Русский

Объединение по x∈s замытий {x} равно s тогда и только тогда, когда s стабильно по специализации.

LaTeX

$$$\left(\bigcup_{x \in s} \overline{\{x\}}\right) = s \iff StableUnderSpecialization(s)$$$

Lean4

theorem Union_closure_singleton_eq_iff {s : Set X} : (⋃ x ∈ s, closure { x }) = s ↔ StableUnderSpecialization s :=
  show _ ↔ IsLowerSet s by simp only [closure_singleton_eq_Iic, ← lowerClosure_eq, coe_lowerClosure]

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