setOf_isClosed_eq_range_closure — Mathlib

English

The set of closed elements for c is exactly the image (range) of c.

Русский

Множество замкнутых элементов для c ровно образ C.

LaTeX

$$$\\\\{ x : {\\\\alpha} \\\\mid c.IsClosed x \\\\} = \\\\mathrm{range} (c)$$$

Lean4

/-- The set of closed elements for `c` is exactly its range. -/
theorem setOf_isClosed_eq_range_closure : {x | c.IsClosed x} = Set.range c := by ext x;
  exact ⟨fun hx ↦ ⟨x, hx.closure_eq⟩, by rintro ⟨y, rfl⟩; exact c.isClosed_closure _⟩

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