subsingleton — Mathlib

English

If a function f: α → β is 0-antilipschitz, then α must be a singleton (subsingleton).

Русский

Если функция f: α → β является 0‑антиллипшиц, то множество α является синглтоном (одиночным).

LaTeX

$$$\operatorname{AntilipschitzWith}(0,f) \Rightarrow \operatorname{Subsingleton} \alpha$$$

Lean4

/-- If `f : α → β` is `0`-antilipschitz, then `α` is a `subsingleton`. -/
protected theorem subsingleton {α β} [EMetricSpace α] [PseudoEMetricSpace β] {f : α → β} (h : AntilipschitzWith 0 f) :
    Subsingleton α :=
  ⟨fun x y => edist_le_zero.1 <| (h x y).trans_eq <| zero_mul _⟩

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