English
Adjoining S and then T, and restricting scalars to F, gives the same as adjoining S ∪ T: adjoin(adjoin F S, T) restricted to F equals adjoin F (S ∪ T).
Русский
Добавление S затем T, с ограничением скаляров к F, эквивалентно добавлению S ∪ T: adjoin(adjoin F S, T) ≅ adjoin F (S ∪ T).
LaTeX
$$$(\operatorname{adjoin}(\operatorname{adjoin}_F S) T)\restrictionScalars _ = \operatorname{adjoin}_F (S \cup T)$$$
Lean4
/-- Adjoining S and then T is the same as adjoining `S ∪ T`. -/
theorem adjoin_adjoin_left (T : Set E) : (adjoin (adjoin F S) T).restrictScalars _ = adjoin F (S ∪ T) :=
by
rw [SetLike.ext'_iff]
change (adjoin (adjoin F S) T : Set E) = _
apply subset_antisymm <;> rw [adjoin_subset_adjoin_iff] <;> constructor
· rintro _ ⟨⟨x, hx⟩, rfl⟩; exact adjoin.mono _ _ _ Set.subset_union_left hx
· exact subset_adjoin_of_subset_right _ _ Set.subset_union_right
· exact Set.range_subset_iff.mpr fun f ↦ Subfield.subset_closure (.inl ⟨f, rfl⟩)
·
exact
Set.union_subset (fun x hx ↦ Subfield.subset_closure <| .inl ⟨⟨x, Subfield.subset_closure (.inr hx)⟩, rfl⟩)
(fun x hx ↦ Subfield.subset_closure <| .inr hx)
