not_irreducible_of_aleph0_le

Mathlib.SetTheory.Cardinal.Divisibility

URI: https://scilib.ai/kg/mathlib#Cardinal.not_irreducible_of_aleph0_le

← MathLib Explorer

English

If aleph_0 ≤ a, then a is not irreducible.

Русский

Если aleph_0 ≤ a, то a неразложимо.

LaTeX

$$$\aleph_0 \le a \Rightarrow \lnot \mathrm{Irreducible}(a)$$$

Lean4

theorem not_irreducible_of_aleph0_le (ha : ℵ₀ ≤ a) : ¬Irreducible a :=
  by
  rw [irreducible_iff, not_and_or]
  refine Or.inr fun h => ?_
  simpa [mul_aleph0_eq ha, isUnit_iff, (one_lt_aleph0.trans_le ha).ne', one_lt_aleph0.ne'] using @h a ℵ₀

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

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

Разделы

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

Аффилиация

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