English
Let S be a set of intermediate fields F with a defining property p, contained in A over ℚ, and let T be a finite set of elements of A such that each F ∈ S equals the field generated by a single element over ℚ, namely F = ℚ⟮x⟯ for some x ∈ T. Then the collection S is finite.
Русский
Пусть S — множество промежуточных полей F, принадлежащих A над ℚ, удовлетворяющее некоему свойству p, и пусть T — конечное множество элементов из A так, что для каждого F ∈ S существует x ∈ T с F = ℚ⟮x⟯. Тогда множество S конечно.
LaTeX
$$$$\\text{If } S \\subseteq \\{F : \\text{IntermediateField}_{\\mathbb{Q}}(A) \\mid p(F)\\} \\text{ and } T \\text{ is finite with } (\\forall F \\in S)(\\exists x \\in T\\; F = \\mathbb{Q}(x)), \\text{ then } S \\text{ is finite.}$$$$
Lean4
theorem finite_of_finite_generating_set {p : IntermediateField ℚ A → Prop}
(S : Set { F : IntermediateField ℚ A // p F }) {T : Set A} (hT : T.Finite) (h : ∀ F ∈ S, ∃ x ∈ T, F = ℚ⟮x⟯) :
S.Finite := by
rw [← Set.finite_coe_iff] at hT
refine
Set.finite_coe_iff.mp <|
Finite.of_injective (fun ⟨F, hF⟩ ↦ (⟨(h F hF).choose, (h F hF).choose_spec.1⟩ : T)) (fun _ _ h_eq ↦ ?_)
rw [Subtype.ext_iff, Subtype.ext_iff]
convert congr_arg (ℚ⟮·⟯) (Subtype.mk_eq_mk.mp h_eq)
all_goals exact (h _ (Subtype.mem _)).choose_spec.2
