mk_int — Mathlib

English

A convenient constructor for IsFiltration when the index is the integers: F(n) = F(n-1) for all n.

Русский

Удобный конструктор IsFiltration, когда индекс целые числа: F(n) = F(n-1) для каждого n.

LaTeX

$$$\\text{IsFiltration.mk_int}(F,\\,\\text{mono}) : \\text{IsFiltration } F (n \\mapsto F(n-1))$$$

Lean4

/-- A convenience constructor for `IsFiltration` when the index is the integers. -/
theorem mk_int (F : ℤ → σ) (mono : Monotone F) : IsFiltration F (fun n ↦ F (n - 1))
    where
  mono := mono
  is_le lt := mono (Int.le_sub_one_of_lt lt)
  is_sup _ j hi := hi (j - 1) (sub_one_lt j)

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