mem_iInf — Mathlib

English

An element x belongs to the infimum of a family of ideals I iff it belongs to every I in the family.

Русский

Элемент x принадлежит пересечению всей семьи идеалов I i тогда и только тогда, когда он принадлежит каждому I i.

LaTeX

$$$x \\in \\;iInf I \\iff \\forall i, x \\in I(i)$$$

Lean4

theorem mem_iInf {ι : Type*} {I : ι → TwoSidedIdeal R} {x : R} : x ∈ iInf I ↔ ∀ i, x ∈ I i :=
  show (∀ _, _) ↔ _ by simp [mem_iff]

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