iInf_toSubsemiring — Mathlib

English

For any S: ι → Subalgebra R A, the infimum toSubsemiring equals the infimum of the subsemirings: (iInf S).toSubsemiring = ⨅ i, (S i).toSubsemiring.

Русский

Для семейства подпалгебр S_i выполняется: (iInf S).toSubsemiring = ⨅ i, (S i).toSubsemiring.

LaTeX

$$$\left(\bigwedge_i S_i\right).toSubsemiring = \bigwedge_i (S_i.toSubsemiring)$$$

Lean4

@[simp]
theorem iInf_toSubsemiring {ι : Sort*} (S : ι → Subalgebra R A) : (iInf S).toSubsemiring = ⨅ i, (S i).toSubsemiring :=
  by simp only [iInf, sInf_toSubsemiring, ← Set.range_comp, Function.comp_def]

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