irreducibleSpace — Mathlib

English

If s is irreducible, then the subtype s = {x ∈ X | x ∈ s} is irreducible.

Русский

Если s неразложимо, то подпространство-тип s = {x ∈ X | x ∈ s} неразложимо.

LaTeX

$$$\mathrm{IsIrreducible}(s) \rightarrow \mathrm{IrreducibleSpace}(s.\mathrm{Elem})$$$

Lean4

theorem irreducibleSpace (h : IsIrreducible s) : IrreducibleSpace s
    where
  isPreirreducible_univ := (Subtype.preirreducibleSpace h.isPreirreducible).isPreirreducible_univ
  toNonempty := h.nonempty.to_subtype

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