English
Let i be a fixed index. The filtrations indexed by j with j < i form a directed system under inclusion; that is, for any j1, j2 < i there exists a j3 < i such that j1 ≤ j3 and j2 ≤ j3, and the corresponding filtrations are nested: filtration(j1) ⊆ filtration(j3) and filtration(j2) ⊆ filtration(j3).
Русский
Пусть i фиксировано. Фильтрации, индексируемые всеми j < i, образуют направленную систему по включению: для любых j1, j2 < i существует j3 < i с j1 ≤ j3 и j2 ≤ j3, и соответствующие фильтрации удовлетворяют вложению filtration(j1) ⊆ filtration(j3) и filtration(j2) ⊆ filtration(j3).
LaTeX
$$$\\operatorname{Directed}(\\le)\\Big(\\lambda j: Iio(i).\\, \\mathrm{filtration}(j).1\\Big)$$$
Lean4
theorem directed_filtration : Directed (· ≤ ·) fun j : Iio i ↦ filtration j.1 :=
(filtration.monotone.comp <| Subtype.mono_coe _).directed_le
