toSubalgebra_iSup_of_directed — Mathlib

English

For a directed family t of intermediate fields, the underlying subalgebra of iSup t is the supremum of the subalgebras of each t_i: (iSup t).toSubalgebra = ⨆ i, (t i).toSubalgebra.

Русский

Для направленной семьи промежуточных полей A_i имеем: (iSup t).toSubalgebra = ⨆ i (t_i).toSubalgebra.

LaTeX

$$$(\mathrm{iSup}\ t).\text{toSubalgebra} = \big(\bigsqcup_i (t_i).toSubalgebra\big)$$$

Lean4

theorem toSubalgebra_iSup_of_directed (dir : Directed (· ≤ ·) t) : (iSup t).toSubalgebra = ⨆ i, (t i).toSubalgebra :=
  by
  cases isEmpty_or_nonempty ι
  · simp_rw [iSup_of_empty, bot_toSubalgebra]
  · exact SetLike.ext' ((coe_iSup_of_directed dir).trans (Subalgebra.coe_iSup_of_directed dir).symm)

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