mapDomain_nonneg

Mathlib.Data.Finsupp.Order

URI: https://scilib.ai/kg/mathlib#Finsupp.mapDomain_nonneg

English

If g is nonnegative, then g.mapDomain f is nonnegative as well.

Русский

Если g ≥ 0, то g.mapDomain f ≥ 0.

LaTeX

$$0 \le g \Rightarrow 0 \le g.mapDomain f$$

Lean4

theorem mapDomain_nonneg (hg : 0 ≤ g) : 0 ≤ g.mapDomain f := by simpa using mapDomain_mono hg

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru