mem_sInf — Mathlib

English

A element x belongs to the infimum of a set S of subalgebras iff x belongs to every member of S.

Русский

Элемент x принадлежит инфимума множества подпалгебр S тогда и только тогда, когда x принадлежит каждой подпалгебре из S.

LaTeX

$$$ x \\in \\mathrm{sInf}(S) \\; \\Leftrightarrow\\; \\forall p \\in S, \\; x \\in p $$$

Lean4

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

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