coe_sInf — Mathlib

English

The carrier of the infimum sInf S is the intersection of the carriers of the members of S.

Русский

Облако множества, порождаемого инфимумом sInf S, равно пересечению носителей элементов S.

LaTeX

$$$\uparrow(\mathrm{sInf}(S)) = \bigwedge_{s \in S} (s : Set M)$$$

Lean4

@[simp, norm_cast]
theorem coe_sInf (S : Set (ClosedSubmodule R M)) : ↑(sInf S) = ⨅ s ∈ S, (s : Set M) := by simp [← coe_toSubmodule]

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