adjoin_le_iff — Mathlib

English

For any S ⊆ E and T an intermediate field, adjoin F S ≤ T if and only if S ⊆ T.

Русский

Для любого S ⊆ E и T∈ IntermediateField, adjoin F S ≤ T тогда и только тогда, когда S ⊆ T.

LaTeX

$$adjoin F S \le T \iff S \subseteq T$$

Lean4

@[simp]
theorem adjoin_le_iff {S : Set E} {T : IntermediateField F E} : adjoin F S ≤ T ↔ S ⊆ T :=
  ⟨fun H => le_trans (le_trans Set.subset_union_right Subfield.subset_closure) H, fun H =>
    (@Subfield.closure_le E _ (Set.range (algebraMap F E) ∪ S) T.toSubfield).mpr
      (Set.union_subset (IntermediateField.set_range_subset T) H)⟩

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