mem_sInf — Mathlib

English

For a set s of ideals, x ∈ sInf s iff x ∈ I for all I ∈ s.

Русский

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

LaTeX

$$$x \\in \\mathrm{sInf}\,s \\iff \\forall I \\in s,\, x \\in I$$$

Lean4

theorem mem_sInf {s : Set (Ideal R)} {x : R} : x ∈ sInf s ↔ ∀ ⦃I⦄, I ∈ s → x ∈ I :=
  ⟨fun hx I his => hx I ⟨I, iInf_pos his⟩, fun H _I ⟨_J, hij⟩ => hij ▸ fun _S ⟨hj, hS⟩ => hS ▸ H hj⟩

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