English
The class of filtrations on (Ω, m) indexed by a preorder ι forms a lattice under pointwise order. The join (supremum) of two filtrations f and g is defined by taking at each index i the supremum of the two σ-algebras f(i) and g(i). Consequently, f ⊔ g is a filtration, and it is the least upper bound of f and g: f ≤ f ⊔ g, g ≤ f ⊔ g, and if h is a filtration with f ≤ h and g ≤ h, then f ⊔ g ≤ h. Similarly, the meet f ⊓ g is defined pointwise by f(i) ⊓ g(i).
Русский
Множество фильтраций над (Ω, m), индексируемых частичным порядком ι, образует решётку относительно покомпонентного упорядочения. Объединение двух фильтраций f и g задаётся на каждом индексе i через верхнюю границу σ‑алгебт: (f ⊔ g)(i) = f(i) ⊔ g(i). Следовательно, f ⊔ g является фильтрацией и является наименьшей верхней границей двух данных фильтраций: f ≤ f ⊔ g, g ≤ f ⊔ g, и если h — фильтрация с f ≤ h и g ≤ h, то f ⊔ g ≤ h. Аналогично определено пересечение f ⊓ g по точкам: (f ⊓ g)(i) = f(i) ⊓ g(i).
LaTeX
$$$\\forall f,g : Filtration ι m,\\; (f \\sqcup g) \\text{ is a filtration with } ((f \\sqcup g)(i)) = f(i) \\vee g(i) \\\\\\quad \\&\\; f \\le f \\sqcup g,\\; g \\le f \\sqcup g,\\;\\; \\text{and if } h \\text{ is a filtration with } f \\le h \\text{ and } g \\le h, \\text{ then } f \\sqcup g \\le h. \\\\ \\\\quad \\text{Similarly } (f \\sqcap g)(i) = f(i) \\wedge g(i).$$$
Lean4
instance : Max (Filtration ι m) :=
⟨fun f g =>
{ seq := fun i => f i ⊔ g i
mono' := fun _ _ hij => sup_le ((f.mono hij).trans le_sup_left) ((g.mono hij).trans le_sup_right)
le' := fun i => sup_le (f.le i) (g.le i) }⟩
