nonempty

Mathlib.Topology.Irreducible

URI: https://scilib.ai/kg/mathlib#IsIrreducible.nonempty

English

If s is irreducible, then s is nonempty.

Русский

Если s неразложимо, то оно непусто.

LaTeX

$$$\\operatorname{IsIrreducible}(s) \\rightarrow s \\neq \\emptyset$$$

Lean4

theorem nonempty (h : IsIrreducible s) : s.Nonempty :=
  h.1

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

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

Разделы

Аффилиация

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