coe_sInf — Mathlib

English

In a family of subalgebras, the underlying set of the infimum equals the intersection of the underlying sets of each member.

Русский

Для семейства подпалгебр основание инфимума равно пересечению оснований.

LaTeX

$$$ (\\iInf i, S_i).toSubmodule = \\bigcap_i S_i.toSubmodule $$$

Lean4

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

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