mapDomain_nonpos

Mathlib.Data.Finsupp.Order

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

English

If g ≤ 0, then g.mapDomain f ≤ 0.

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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