radical_le_coatom

Mathlib.Order.Radical

URI: https://scilib.ai/kg/mathlib#Order.radical_le_coatom

English

If a is a coatom in a complete lattice α, then radical(α) ≤ a.

Русский

Если a — коатом в полной решётке α, то radical(α) ≤ a.

LaTeX

$$$\mathrm{IsCoatom}(a) \Rightarrow \operatorname{radical}(\alpha) \le a.$$$

Lean4

theorem radical_le_coatom {a : α} (h : IsCoatom a) : radical α ≤ a :=
  biInf_le _ h

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

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

Разделы

Аффилиация

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