isIrreducible — Mathlib

English

If s is an irreducible closed subset of α, then s regarded as a set is irreducible.

Русский

Если s является неразложимым замкнутым подмножеством α, то рассматриваемое как множество s является неразложимым.

LaTeX

$$$\forall s \in \mathrm{IrreducibleCloseds}(\alpha):\ IsIrreducible (s : \mathrm{Set}(\alpha)).$$$

Lean4

theorem isIrreducible (s : IrreducibleCloseds α) : IsIrreducible (s : Set α) :=
  s.is_irreducible'

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