isClosed_of_mem_irreducibleComponents

English

If s is a member of irreducibleComponents(X), then s is closed in X.

Русский

Если s принадлежит irreducibleComponents(X), то s закрыто в X.

LaTeX

$$$s \\in \\operatorname{irreducibleComponents}(X) \\Rightarrow \\operatorname{IsClosed}(s)$$$

Lean4

@[stacks 004W "(2)"]
theorem isClosed_of_mem_irreducibleComponents (s) (H : s ∈ irreducibleComponents X) : IsClosed s :=
  by
  rw [← closure_eq_iff_isClosed, eq_comm]
  exact subset_closure.antisymm (H.2 H.1.closure subset_closure)

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