gc

Mathlib.Topology.Order.HullKernel

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

← MathLib Explorer

English

If T is order-generating, then kernel(hull(T, a)) = a for any a ∈ α.

Русский

Если T порождает порядок, то для любого a выполняется kernel(hull(T, a)) = a.

LaTeX

$$$\\operatorname{kernel}(\\mathrm{hull}(T, a)) = a$ (assuming $T$ is order-generates).$$

Lean4

theorem gc : GaloisConnection (α := Set T) (β := αᵒᵈ) (fun S => toDual (kernel S)) (fun a => hull T (ofDual a)) :=
  fun S a => by simp [Set.subset_def]

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

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

Разделы

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

Аффилиация

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