map_cast_int_atTop — Mathlib

English

The natural-to-integer cast sends the atTop filter to atTop.

Русский

Отображение из натуральных чисел в целые числа отправляет фильтр atTop в atTop.

LaTeX

$$$\mathrm{Eq}\left( \mathrm{Filter.map}\ \mathrm{Nat.cast}\ \mathrm{Filter.atTop}, \mathrm{Filter.atTop} \right)$$$

Lean4

@[simp]
theorem _root_.Nat.map_cast_int_atTop : map ((↑) : ℕ → ℤ) atTop = atTop :=
  by
  refine map_atTop_eq_of_gc_preorder (fun _ _ ↦ Int.ofNat_le.2) 0 fun n hn ↦ ?_
  lift n to ℕ using hn
  exact ⟨n, rfl, fun _ ↦ Int.ofNat_le⟩

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