map_div_atTop_eq_nat — Mathlib

English

For k ∈ ℕ, k > 0, the map a ↦ a / k sends atTop to atTop; i.e., dividing by a positive constant preserves the atTop filter.

Русский

Для k ∈ ℕ, k > 0, отображение a ↦ a / k переводит atTop в atTop; деление на положительное число сохраняет фильтр atTop.

LaTeX

$$$$\text{map}(\lambda a. a / k)\operatorname{atTop} = \operatorname{atTop} \quad (k > 0)$$$$

Lean4

theorem map_div_atTop_eq_nat (k : ℕ) (hk : 0 < k) : map (fun a => a / k) atTop = atTop :=
  map_atTop_eq_of_gc (fun b => k * b + (k - 1)) 1 (fun _ _ h => Nat.div_le_div_right h)
    (fun a b _ => by rw [Nat.div_le_iff_le_mul_add_pred hk]) fun b _ => by
    rw [Nat.mul_add_div hk, Nat.div_eq_of_lt, Nat.add_zero]; cutsat

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