instIsCompactlyGenerated — Mathlib

English

The lattice of intermediate fields is compactly generated by the compact elements F⟮x⟯ and finite joins adjoin F S.

Русский

Решетка промежуточных полей компактно порождается компактными элементами вида F⟮x⟯ и конечными соединениями adjoin.

LaTeX

$$IsCompactlyGenerated (IntermediateField F E)$$

Lean4

/-- The lattice of intermediate fields is compactly generated. -/
instance : IsCompactlyGenerated (IntermediateField F E) :=
  ⟨fun s =>
    ⟨(fun x => F⟮x⟯) '' s,
      ⟨by rintro t ⟨x, _, rfl⟩; exact adjoin_simple_isCompactElement x,
        sSup_image.trans <|
          (biSup_adjoin_simple _).trans <| le_antisymm (adjoin_le_iff.mpr le_rfl) <| subset_adjoin F (s : Set E)⟩⟩⟩

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