continuous_choose — Mathlib

English

Let p be a prime. For every k ∈ ℕ the map x ↦ x choose k is continuous on ℤ_p.

Русский

Пусть p — простое число. Для каждого k ∈ ℕ отображение x ↦ C(x,k) непрерывно на ℤ_p.

LaTeX

$$$$ \forall p \text{ prime}, \forall k \in \\mathbb{N}, \\; x \\mapsto {x \\choose k} : \\mathbb{Z}_p \\to \\mathbb{Z}_p \\text{ is continuous}. $$$$

Lean4

@[fun_prop]
theorem continuous_choose (k : ℕ) : Continuous (fun x : ℤ_[p] ↦ Ring.choose x k) :=
  by
  simp only [Ring.choose]
  fun_prop

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