map_add_atTop_eq — Mathlib

English

Adding a fixed element to all elements in a directed ordered set preserves the atTop filter.

Русский

Прибавление фиксированного элемента ко всем элементам направленного упорядоченного множества сохраняет фильтр atTop.

LaTeX

$$$\mathrm{map}(a \mapsto a+k)\ \mathrm{atTop} = \mathrm{atTop}$$$

Lean4

theorem map_add_atTop_eq [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] [IsDirected α (· ≤ ·)] (k : α) :
    map (fun a => a + k) atTop = atTop :=
  map_atTop_eq_of_gc (fun a => a - k) 0 add_left_mono (by simp [le_sub_iff_add_le]) (by simp)

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