English
Let F be a field and E a field with an F-algebra structure. For any subset S ⊆ E and any x ∈ E, the intermediate field generated by S together with x after adjoining S is the same as the field generated by S together with x, i.e., adjoin_F(insert x (adjoin_F S)) = adjoin_F(insert x S).
Русский
Пусть F — поле, E — расширение над F, и S ⊆ E. Для любого x ∈ E подполе, порождаемое S и x, равно полю, порождаемому S и x, то есть adjoin_F(insert x (adjoin_F S)) = adjoin_F(insert x S).
LaTeX
$$$\\\\operatorname{adjoin}_F(\\\\operatorname{insert} x (\\\\operatorname{adjoin}_F S)) = \\\\operatorname{adjoin}_F(\\\\operatorname{insert} x S).$$$
Lean4
@[simp]
theorem adjoin_insert_adjoin (x : E) : adjoin F (insert x (adjoin F S : Set E)) = adjoin F (insert x S) :=
le_antisymm
(adjoin_le_iff.mpr
(Set.insert_subset_iff.mpr
⟨subset_adjoin _ _ (Set.mem_insert _ _),
adjoin_le_iff.mpr (subset_adjoin_of_subset_right _ _ (Set.subset_insert _ _))⟩))
(by grw [← subset_adjoin])
