support_monotone

Mathlib.Data.DFinsupp.Order

URI: https://scilib.ai/kg/mathlib#DFinsupp.support_monotone

← MathLib Explorer

English

The support map is monotone: if f ≤ g then the support of f is contained in the support of g.

Русский

Отображение поддержки монотонно: если f ≤ g, то supp(f) ⊆ supp(g).

LaTeX

$$Monotone(\\mathrm{support})$$

Lean4

theorem support_monotone : Monotone (support (ι := ι) (β := α)) := fun f g h a ha ↦ by
  rw [mem_support_iff, ← pos_iff_ne_zero] at ha ⊢; exact ha.trans_le (h _)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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