English
The InfSet (greatest lower bound) of a family of filtrations is again an I-filtration with N given by the infimum of their N-components.
Русский
Обобщённое InfSet над семейством фильтраций снова является I-фильтрацией и имеет N, равный пересечению их N-компонент.
LaTeX
$$N = sInf (N '' S)$$
Lean4
/-- The `sInf` of a family of `I.Filtration`s is an `I.Filtration`. -/
instance : InfSet (I.Filtration M) :=
⟨fun S =>
{ N := sInf (Ideal.Filtration.N '' S)
mono := fun i => by
apply sInf_le_sInf_of_isCoinitialFor _
rintro _ ⟨⟨_, F, hF, rfl⟩, rfl⟩
exact ⟨_, ⟨⟨_, F, hF, rfl⟩, rfl⟩, F.mono i⟩
smul_le := fun i => by
rw [sInf_eq_iInf', iInf_apply, iInf_apply]
refine smul_iInf_le.trans ?_
apply iInf_mono _
rintro ⟨_, F, hF, rfl⟩
exact F.smul_le i }⟩
