biSup_adjoin_simple — Mathlib

English

Let S be a subset of E. The smallest intermediate field of E over F that contains S is the join (supremum) of all subfields generated by the individual elements of S; equivalently, adjoin F S equals the supremum of the fields F⟨x⟩ as x ranges over S.

Русский

Пусть S ⊆ E. Наименьшее подполе над F, содержащее S, равно наибольшему объединению всех подполей, порожденных каждым элементом S; то есть adjoin_F(S) является объединением F⟨x⟩ по x ∈ S.

LaTeX

$$$\displaystyle \bigvee_{x \in S} F\langle x \rangle = \operatorname{adjoin}_F S$$$

Lean4

theorem biSup_adjoin_simple : ⨆ x ∈ S, F⟮x⟯ = adjoin F S := by rw [← iSup_subtype'', ← gc.l_iSup, iSup_subtype''];
  congr; exact S.biUnion_of_singleton

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