English
If i is a successor prelimit, then the supremum over all j < i of filtration(j) equals filtration(i).
Русский
Если i является пределом предельной последовательности-суффикс, то наибольший предел фильтраций filtration(j) по j<i равен filtration(i).
LaTeX
$$$\\bigvee_{j\\in Iio(i)} \\mathrm{filtration}(j) = \\mathrm{filtration}(i) \\quad \\text{when } i \\text{ is a successor prelimit.}$$$
Lean4
theorem iSup_filtration : ⨆ j : Iio i, filtration j = filtration i :=
by
cases i
· rw [← range_coe, iSup_range']; exact iSup_adjoin_eq_top
refine (iSup_le fun j ↦ filtration.monotone (mem_Iio.1 j.2).le).antisymm (adjoin_le_iff.2 ?_)
rintro _ ⟨j, hj, rfl⟩
refine le_iSup (α := IntermediateField F E) _ ⟨j⁺, ?_⟩ (subset_adjoin F _ ?_)
exacts [⟨j, lt_succ j, rfl⟩, hi.succ_lt (coe_lt_coe.mpr hj)]
