English
The collection of filtrations on Ω with measurable space m forms a complete lattice under the pointwise order: join and meet are defined pointwise by the lattice operations on each level, and top and bottom elements exist as the universal filtration and the trivial filtration, respectively.
Русский
Множество фильтраций над Ω с пространством измеримости m образует полную решётку: операции объединения и пересечения задаются по точкам уровня i, верхняя и нижняя границы существуют как туманная и тривиальная фильтрации.
LaTeX
$$$\\text{Filtration } ι m \\text{ is a complete lattice with } (f \\lor g)(i)=f(i)\\lor g(i),\\; (f \\land g)(i)=f(i)\\land g(i),\\; \\top(i)=\\top,\\; \\bot(i)=\\bot.$$$
Lean4
noncomputable instance : InfSet (Filtration ι m) :=
⟨fun s =>
{ seq := fun i => if Set.Nonempty s then sInf ((fun f : Filtration ι m => f i) '' s) else m
mono' := fun i j hij => by
by_cases h_nonempty : Set.Nonempty s
swap; · simp only [h_nonempty, if_false, le_refl]
simp only [h_nonempty, if_true, le_sInf_iff, Set.mem_image, forall_exists_index, and_imp,
forall_apply_eq_imp_iff₂]
refine fun f hf_mem => le_trans ?_ (f.mono hij)
have hfi_mem : f i ∈ (fun g : Filtration ι m => g i) '' s := ⟨f, hf_mem, rfl⟩
exact sInf_le hfi_mem
le' := fun i => by
by_cases h_nonempty : Set.Nonempty s
swap; · simp only [h_nonempty, if_false, le_refl]
simp only [h_nonempty, if_true]
obtain ⟨f, hf_mem⟩ := h_nonempty
exact le_trans (sInf_le ⟨f, hf_mem, rfl⟩) (f.le i) }⟩
