English
For each i, the subfield obtained by adjoining the images of φ up to i coincides with the adjoin of the images up to i restricted to the i-th stage.
Русский
Для каждого i подполе, порождаемое образами φ до i, совпадает с порождаемым образом в соответствующей стадии.
LaTeX
$$$$\\operatorname{adjoin}_F\\big(\\operatorname{image}(\\varphi\,|\\, \\mathrm{Iio}(i))\\big)=\\operatorname{adjoin}_F\\big(\\operatorname{image}(\\varphi)(\\mathrm{Iio}(i))\\big)$$$$
Lean4
theorem adjoin_image_leastExt (i : ι) : E⟮<i⟯ = adjoin F (b '' Iio (φ i)) :=
by
refine le_antisymm (adjoin.mono _ _ _ ?_) (adjoin_le_iff.mpr ?_)
· rw [image_comp]; apply image_mono; rintro _ ⟨j, hj, rfl⟩; exact strictMono_leastExt hj
· rintro _ ⟨j, hj, rfl⟩; contrapose! hj; exact ((isLeast_leastExt i).2 hj).not_gt
