adjoin_univ

Mathlib.FieldTheory.IntermediateField.Adjoin.Defs

URI: https://scilib.ai/kg/mathlib#IntermediateField.adjoin_univ

← MathLib Explorer

English

Adjoining the universal set yields the top intermediate field: adjoin F Set.univ = ⊤.

Русский

При адьюнте все множества получается верхнее поле: adjoin F Set.univ = ⊤.

LaTeX

$$$\operatorname{adjoin}_F(\mathrm{Set.univ}) = \top$$$

Lean4

@[simp]
theorem adjoin_univ (F E : Type*) [Field F] [Field E] [Algebra F E] : adjoin F (Set.univ : Set E) = ⊤ :=
  eq_top_iff.mpr <| subset_adjoin _ _

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

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

Разделы

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

Аффилиация

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