ideal_biInf — Mathlib

English

For a finite set s and a family I, the ideal of the biInf (intersection over i in s) equals the intersection of the corresponding ideals.

Русский

Для конечного множества s идеал пересечения по i в s равен пересечению соответствующих идеалов.

LaTeX

$$$(\bigwedge_{i \in s} I(i)).ideal = \bigwedge_{i \in s} (I(i).ideal) $$$

Lean4

@[simp]
theorem ideal_biInf {ι : Type*} (I : ι → IdealSheafData X) {s : Set ι} (hs : s.Finite) :
    (⨅ i ∈ s, I i).ideal = ⨅ i ∈ s, (I i).ideal :=
  by
  refine hs.induction_on _ (by simp) fun {i s} his hs e ↦ ?_
  simp only [iInf_insert, e, ideal_inf]

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