mem_iInf — Mathlib

English

The image of the infimum over a set S of subalgebras equals the infimum of the images.

Русский

Образ инфимума над множеством S подпалгебр равен инфимуму образов.

LaTeX

$$$ (sInf S).toNonUnitalSubsemiring = sInf (NonUnitalSubalgebra.toNonUnitalSubsemiring '' S) $$$

Lean4

theorem mem_iInf {ι : Sort*} {S : ι → NonUnitalSubalgebra R A} {x : A} : (x ∈ ⨅ i, S i) ↔ ∀ i, x ∈ S i := by
  simp only [iInf, mem_sInf, Set.forall_mem_range]

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