coe_iInf — Mathlib

English

For a family f: I → ClosedSubmodule(R,M), the carrier of the infimum over i equals the infimum of the carriers: ↑(iInf f) = iInf i, (f i : Set M).

Русский

Для семейства f: I → ClosedSubmodule(R,M) носитель инфимума равен инфимума носителей: ↑(iInf f) = iInf i, (f i : Set M).

LaTeX

$$$\uparrow(\mathrm{iInf}\, f) = \mathrm{iInf}_{i} (f(i) : Set M)$$$

Lean4

@[simp, norm_cast]
theorem coe_iInf (f : ι → ClosedSubmodule R M) : ↑(⨅ i, f i) = ⨅ i, (f i : Set M) := by simp [← coe_toSubmodule]

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