gc — Mathlib · SciLib

English

There is a Galois connection between adjoin F and the coe map; i.e., for S ⊆ E and an intermediate field T, adjoin F S ≤ T if and only if S ⊆ T (as a subset of E).

Русский

Существует Galois связь между adjoin F и отображением коe; то есть для S ⊆ E и T промежуточного поля: adjoin F S ≤ T тогда и только тогда, когда S ⊆ T.

LaTeX

$$GaloisConnection (adjoin F) (\ assum e x : IntermediateField F E) => (x : Set E) := adjoin_le_iff$$

Lean4

theorem gc :
    GaloisConnection (adjoin F : Set E → IntermediateField F E) (fun (x : IntermediateField F E) => (x : Set E)) :=
  fun _ _ => adjoin_le_iff

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