sSup_def — Mathlib

English

The least upper bound of a set of intermediate fields is the adjoin of the union of their carriers.

Русский

Наименьшее верхнее основание множества промежуточных полей — это адъюнкция объединения их носителей.

LaTeX

$$sSup S = \operatorname{adjoin}_F (⋃_0 (\operatorname SetLike.coe '' S))$$

Lean4

theorem sSup_def (S : Set (IntermediateField F E)) : sSup S = adjoin F (⋃₀ (SetLike.coe '' S)) :=
  rfl

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