irreducibleComponent_mem_irreducibleComponents

English

irreducibleComponent(x) is an element of irreducibleComponents(X).

Русский

irreducibleComponent(x) принадлежит irreducibleComponents(X).

LaTeX

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

Lean4

theorem irreducibleComponent_mem_irreducibleComponents (x : X) : irreducibleComponent x ∈ irreducibleComponents X :=
  ⟨isIrreducible_irreducibleComponent, fun _ h₁ h₂ => (eq_irreducibleComponent h₁.2 h₂).le⟩

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