coeFn_sup — Mathlib

English

For filtrations f and g, the underlying function of their supremum coincides with the pointwise supremum of their underlying functions: the coercion to functions satisfies coe(f ⊔ g) = coe(f) ⊔ coe(g).

Русский

Для фильтраций f и g соответствующая отображение их верхнего предела равняется точечному объединению соответствующих отображений: коэрционация lf(f ⊔ g) = lf(f) ⊔ lf(g).

LaTeX

$$$\\operatorname{coe}(f \\sqcup g) = \\operatorname{coe}(f) \\sqcup \\operatorname{coe}(g).$$$

Lean4

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

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