iSup_adjoin_eq_top — Mathlib

English

The supremum (over i) of the subfields adjoined by the indexed images equals the top field.

Русский

Наибольший предел (по i) полей, порождаемых изображениями, равен верхнему полю.

LaTeX

$$$$\\big\\lceil \\operatorname{adjoin}_F(\\text{images up to } i)\\big\\rceil_{i\\in ι} = \\top$$$$

Lean4

theorem iSup_adjoin_eq_top : ⨆ i : ι, E⟮<i⟯ = ⊤ :=
  by
  simp_rw [adjoin_image_leastExt, eq_top_iff, ← adjoin_basis_eq_top, adjoin_le_iff]
  rintro _ ⟨i, rfl⟩
  refine le_iSup (α := IntermediateField F E) _ (i⁺) (subset_adjoin _ _ ⟨i, ?_, rfl⟩)
  exact (lt_succ i).trans_le strictMono_leastExt.le_apply

Похожие утверждения