English
The InfSet construction provides the infimum of a set of filtrations: for a nonempty S, (instInfSet.sInf S)(i) = sInf { f(i) : f ∈ S }, and if S is empty it returns the base σ-algebra m.
Русский
InfSet задаёт наименьшее основание набора фильтраций: если S непусто, то (instInfSet.sInf S)(i) = inf { f(i) : f ∈ S }, иначе m.
LaTeX
$$$(\\mathrm{instInfSet}.sInf\\ S)(i) = \\begin{cases} \\mathrm{sInf}\\{ f(i) : f \\in S\\}, & S \\neq \\varnothing \\\\ m, & S = \\varnothing \\end{cases}$$$
Lean4
instance : SupSet (Filtration ι m) :=
⟨fun s =>
{ seq := fun i => sSup ((fun f : Filtration ι m => f i) '' s)
mono' := fun i j hij => by
refine sSup_le fun m' hm' => ?_
rw [Set.mem_image] at hm'
obtain ⟨f, hf_mem, hfm'⟩ := hm'
rw [← hfm']
refine (f.mono hij).trans ?_
have hfj_mem : f j ∈ (fun g : Filtration ι m => g j) '' s := ⟨f, hf_mem, rfl⟩
exact le_sSup hfj_mem
le' := fun i => by
refine sSup_le fun m' hm' => ?_
rw [Set.mem_image] at hm'
obtain ⟨f, _, hfm'⟩ := hm'
rw [← hfm']
exact f.le i }⟩
