mem_sInf — Mathlib

English

An element x belongs to sInf S precisely when x belongs to every member of S.

Русский

Элемент x принадлежит sInf S тогда и только тогда, когда x принадлежит каждому элементу из S.

LaTeX

$$$x \in \mathrm{sInf}(S) \quad\Leftrightarrow\quad \forall s \in S,\ x \in s$$$

Lean4

@[simp]
theorem mem_sInf {S : Set (ClosedSubmodule R M)} : x ∈ sInf S ↔ ∀ s ∈ S, x ∈ s := by simp [← SetLike.mem_coe]

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