English
Containment of adjoin F S inside adjoin F' S' is equivalent to the conjunction of range inclusion and S ⊆ adjoin F' S'.
Русский
Вложение adjoin F S в adjoin F' S' эквивалентно сочетанию включения образа и S ⊆ adjoin F' S'.
LaTeX
$$$(\operatorname{adjoin} F S : \text{Set} E) \subseteq (\operatorname{adjoin} F' S') \\iff \\big( \operatorname{range}(\mathrm{algebraMap}_{F,E}) \subseteq \operatorname{adjoin}_{F'} S' \wedge S \subseteq \operatorname{adjoin}_{F'} S' \big)$$$
Lean4
theorem adjoin_subset_adjoin_iff {F' : Type*} [Field F'] [Algebra F' E] {S S' : Set E} :
(adjoin F S : Set E) ⊆ adjoin F' S' ↔ Set.range (algebraMap F E) ⊆ adjoin F' S' ∧ S ⊆ adjoin F' S' :=
⟨fun h => ⟨(adjoin.range_algebraMap_subset _ _).trans h, (subset_adjoin _ _).trans h⟩, fun ⟨hF, hS⟩ =>
(Subfield.closure_le (t := (adjoin F' S').toSubfield)).mpr (Set.union_subset hF hS)⟩
