mem_sInf — Mathlib

English

An element x lies in the infimum sInf S iff x lies in every member of S.

Русский

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

LaTeX

$$$x \\in sInf S \\iff \\forall p \\in S,\\ x \\in p$$$

Lean4

theorem mem_sInf {S : Set (NonUnitalStarSubalgebra R A)} {x : A} : x ∈ sInf S ↔ ∀ p ∈ S, x ∈ p := by
  simp only [← SetLike.mem_coe, coe_sInf, Set.mem_iInter₂]

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