mkOfDiscrete — Mathlib

English

If α has the discrete topology, a bounded function f yields a bounded continuous function.

Русский

Если у α дискретная топология, ограниченная функция f даёт ограниченно непрерывную функцию.

LaTeX

$$$mkOfDiscrete [DiscreteTopology(\alpha)] (f : \alpha \to \beta) (C : \mathbb{R}) (h : ∀ x y, dist(f x) (f y) ≤ C) : \alpha \to^b \beta$$$

Lean4

/-- If a function is bounded on a discrete space, it is automatically continuous,
and therefore gives rise to an element of the type of bounded continuous functions. -/
@[simps]
def mkOfDiscrete [DiscreteTopology α] (f : α → β) (C : ℝ) (h : ∀ x y : α, dist (f x) (f y) ≤ C) : α →ᵇ β :=
  ⟨⟨f, continuous_of_discreteTopology⟩, ⟨C, h⟩⟩

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