subset_adjoin — Mathlib

English

For any finite set s, s is contained in the underlying intermediate field of adjoin_k(s).

Русский

Для любого конечного множества s верно, что s содержится в соответствующем промежуточном поле, полученном как adjoin_k(s).

LaTeX

$$$ s \subseteq (adjoin_k(s)).toIntermediateField. $$$

Lean4

theorem subset_adjoin [IsGalois k K] (s : Set K) [Finite s] : s ⊆ (adjoin k s).toIntermediateField :=
  (IntermediateField.subset_adjoin k s).trans (IntermediateField.le_normalClosure _)

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