mem_sInf — Mathlib

English

For a set S of two-sided ideals, x ∈ sInf S iff x belongs to every I ∈ S.

Русский

Для множества S двусторонних идеалов, x принадлежит sInf S тогда и только тогда, когда x принадлежит каждому I ∈ S.

LaTeX

$$$x \\in sInf S \\iff \\forall I \\in S, x \\in I$$$

Lean4

theorem mem_sInf {S : Set (TwoSidedIdeal R)} {x : R} : x ∈ sInf S ↔ ∀ I ∈ S, x ∈ I :=
  show (∀ _, _) ↔ _ by simp [mem_iff]

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