subset_adjoin_of_subset_left

Mathlib.FieldTheory.IntermediateField.Adjoin.Defs

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

← MathLib Explorer

English

If T is a subfield with T ⊆ F, then T ⊆ adjoin F S.

Русский

Если T ⊆ F, то T ⊆ adjoin F S.

LaTeX

$$$T \subseteq F \Rightarrow T \subseteq \operatorname{adjoin}_F S$$$

Lean4

theorem subset_adjoin_of_subset_left {F : Subfield E} {T : Set E} (HT : T ⊆ F) : T ⊆ adjoin F S := fun x hx =>
  (adjoin F S).algebraMap_mem ⟨x, HT hx⟩

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

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

Разделы

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

Аффилиация

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