coeFn_inf — Mathlib

English

The supremum of a set of filtrations S is the filtration whose i-th level is the supremum (join) of the i-th levels of all filtrations in S: (sSup S)(i) = sSup { f(i) : f ∈ S }.

Русский

Супремум множества фильтраций S есть филтрация, у которой на уровне i выполняется (sSup S)(i) = sup { f(i) : f ∈ S }.

LaTeX

$$$(\\mathrm{sSup}\\ S)(i) = \\mathrm{sSup}\\{ f(i) : f \\in S \\}.$$$

Lean4

@[norm_cast]
theorem coeFn_inf {f g : Filtration ι m} : ⇑(f ⊓ g) = ⇑f ⊓ ⇑g :=
  rfl

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