map_add_atTop_eq_nat — Mathlib

English

For every natural number k, translation by k on the index set does not change the atTop filter: the image of atTop under the map a ↦ a + k is still atTop.

Русский

Для каждого натурального числа k отображение сдвига по индексу: a ↦ a + k сохраняет фильтр atTop: образ atTop под этим отображением равен atTop.

LaTeX

$$$$\operatorname{map}\bigl(\lambda a. a + k\bigr)\operatorname{atTop} = \operatorname{atTop}$$$$

Lean4

theorem map_add_atTop_eq_nat (k : ℕ) : map (fun a => a + k) atTop = atTop :=
  map_atTop_eq_of_gc (· - k) k (fun _ _ h => Nat.add_le_add_right h k) (fun _ _ h => (Nat.le_sub_iff_add_le h).symm)
    fun a h => by rw [Nat.sub_add_cancel h]

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