mem_iInf — Mathlib

English

An element x lies in the infimum of a family of subrings iff x lies in every member of the family.

Русский

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

LaTeX

$$$$x \in iInf S \;\Leftrightarrow\; \forall i, x \in S_i.$$$$

Lean4

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

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