F_lt_le_F — Mathlib

English

In a filtration indexed by a partially ordered set, the lower bound F_lt(i) is less than or equal to F(i).

Русский

В фильтрации, индексированной частично упорядоченным множеством, нижняя граница F_lt(i) не превосходит F(i).

LaTeX

$$$F_{\\text{lt}}(i) \\le F(i)$$$

Lean4

theorem F_lt_le_F (F : ι → σ) (F_lt : outParam <| ι → σ) (i : ι) [IsFiltration F F_lt] : F_lt i ≤ F i :=
  is_sup (F i) i (fun _ hi ↦ IsFiltration.mono (le_of_lt hi))

Похожие утверждения