of_subsingleton — Mathlib

English

If the domain α is a subsingleton, then any map f: α → β is automatically AntilipschitzWith K f for any K.

Русский

Если область определения α является subsingleton’ом, то любая отображение f: α → β автоматически является AntilipschitzWith K f для любого K.

LaTeX

$$$ (\text{Subsingleton } \alpha) \Rightarrow \operatorname{AntilipschitzWith} K f$$$

Lean4

@[nontriviality]
theorem of_subsingleton [Subsingleton α] {K : ℝ≥0} : AntilipschitzWith K f := fun x y => by
  simp only [Subsingleton.elim x y, edist_self, zero_le]

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