coe_sInf — Mathlib

English

The underlying set of the infimum of a set S of subalgebras equals the intersection of the underlying sets of all members: ↑(sInf S) = ⋂ s ∈ S, ↑s.

Русский

Основное множество наименьшего элемента множества подпалгебр равно пересечению множеств всех его элементов: ↑(sInf S) = ⋂ s ∈ S, ↑s.

LaTeX

$$$\uparrow (sInf S) = \bigcap_{s \in S} \uparrow s$$$

Lean4

@[simp, norm_cast]
theorem coe_sInf (S : Set (Subalgebra R A)) : (↑(sInf S) : Set A) = ⋂ s ∈ S, ↑s :=
  sInf_image

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