kernel_hull

Mathlib.Topology.Order.HullKernel

URI: https://scilib.ai/kg/mathlib#PrimitiveSpectrum.kernel_hull

← MathLib Explorer

English

For an order-generating T, kernel(hull(T, a)) equals a for every a ∈ α.

Русский

Для T, порождающего порядок, kernel(hull(T, a)) = a для каждого a ∈ α.

LaTeX

$$$\\ker(\\mathrm{hull}(T, a)) = a$$$

Lean4

theorem kernel_hull (hG : OrderGenerates T) (a : α) : kernel (hull T a) = a :=
  by
  conv_rhs => rw [← OrderDual.ofDual_toDual a, ← (gi hG).l_u_eq a]
  rfl

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

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

Разделы

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

Аффилиация

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