map_sub_atTop_eq — Mathlib

English

Subtracting a fixed element from all elements in a directed ordered set preserves atTop.

Русский

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

LaTeX

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

Lean4

theorem map_sub_atTop_eq [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] [IsDirected α (· ≤ ·)] (k : α) :
    map (fun a => a - k) atTop = atTop := by
  simp_rw [sub_eq_add_neg]
  apply map_add_atTop_eq

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