mem_irreducibleComponent

Mathlib.Topology.Irreducible

URI: https://scilib.ai/kg/mathlib#mem_irreducibleComponent

← MathLib Explorer

English

x is an element of its irreducible component: x ∈ irreducibleComponent(x).

Русский

x принадлежит своей неразложимой компоненте: x ∈ irreducibleComponent(x).

LaTeX

$$$x \\in \\operatorname{irreducibleComponent}(x)$$$

Lean4

@[stacks 004W "(4)"]
theorem mem_irreducibleComponent {x : X} : x ∈ irreducibleComponent x :=
  singleton_subset_iff.1 (irreducibleComponent_property x).2.1

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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