iSup_eq_adjoin — Mathlib

English

Let f: ι → IntermediateField F E. Then the supremum of f equals the adjoin of the union of all f(i): ⨆ i, f(i) = adjoin F (⋃ i, f(i) under the underlying Set).

Русский

Объединение по верхней грани: ⨆ i, f(i) = adjoin F (⋃ i, ⋯).

LaTeX

$$$\\\\bigvee_i f(i) = \\\\operatorname{adjoin}_F (\\\\bigcup_i f(i)).$$$

Lean4

theorem iSup_eq_adjoin {ι} (f : ι → IntermediateField F E) : ⨆ i, f i = adjoin F (⋃ i, f i : Set E) := by
  simp_rw [adjoin_iUnion, adjoin_self]

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