closure_paramSet

Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

URI: https://scilib.ai/kg/mathlib#NumberField.mixedEmbedding.fundamentalCone.closure_paramSet

← MathLib Explorer

English

The same ae-equivalence result for closure and interior of paramSet under the volume measure.

Русский

Та же ae-эквивалентность для closure и interior paramSet относительно объёма.

LaTeX

$$closure(paramSet K) =ᵐ[volume] interior(paramSet K)$$

Lean4

theorem closure_paramSet : closure (paramSet K) = Set.univ.pi fun w ↦ if w = w₀ then Set.Iic 0 else Set.Icc 0 1 := by
  simp [closure_pi_set, apply_ite]

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

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

Разделы

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

Аффилиация

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