adjoin_finite_isCompactElement — Mathlib

English

The lattice of intermediate fields is finitely generated by compact elements coming from singletons and finite adjoins.

Русский

Решетка промежуточных полей порождается конечными компактными элементами, соответствующими одиночным элементам и конечным адъойнам.

LaTeX

$$IsCompactlyGenerated (IntermediateField F E)$$

Lean4

/-- Adjoining a finite subset is compact in the lattice of intermediate fields. -/
theorem adjoin_finite_isCompactElement {S : Set E} (h : S.Finite) : IsCompactElement (adjoin F S) :=
  Finite.coe_toFinset h ▸ adjoin_finset_isCompactElement h.toFinset

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