map_sub_atTop_eq_nat — Mathlib

English

For every k ∈ ℕ, the map a ↦ a − k sends the atTop filter on ℕ to itself: the atTop filter is invariant under subtracting a fixed natural number.

Русский

Для каждого k ∈ ℕ отображение a ↦ a − k сохраняет фильтр atTop на ℕ, т. е. atTop инвариантен относительно вычитания фиксированного натурального числа.

LaTeX

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

Lean4

theorem map_sub_atTop_eq_nat (k : ℕ) : map (fun a => a - k) atTop = atTop :=
  map_atTop_eq_of_gc (· + k) 0 (fun _ _ h => Nat.sub_le_sub_right h _) (fun _ _ _ => Nat.sub_le_iff_le_add) fun b _ =>
    by rw [Nat.add_sub_cancel_right]

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