isIrreducible

Mathlib.Topology.Sober

URI: https://scilib.ai/kg/mathlib#IsGenericPoint.isIrreducible

English

A generic point x of S implies S is irreducible.

Русский

Обобщенная точка x множества S означает, что S неразложимо (ирредуцируема).

LaTeX

$$$ \mathrm{IsGenericPoint}(x,S) \Rightarrow \mathrm{IsIrreducible}(S)$$$

Lean4

protected theorem isIrreducible (h : IsGenericPoint x S) : IsIrreducible S :=
  h.def ▸ isIrreducible_singleton.closure

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru