mapsTo_emetric_closedBall — Mathlib

English

ContinuousOn ((f:α→β) ∘ g) on s is equivalent to ContinuousOn g on s.

Русский

Непрерывность на s композиции ((f) ∘ g) равносильна непрерывности g на s.

LaTeX

$$$\\text{ContinuousOn}((f:\\alpha\\to\\beta) \\circ g)\\; s \\iff \\text{ContinuousOn}\\; g\\; s$$$

Lean4

/-- A dilation maps closed balls to closed balls and scales the radius by `ratio f`. -/
theorem mapsTo_emetric_closedBall (x : α) (r' : ℝ≥0∞) :
    MapsTo (f : α → β) (EMetric.closedBall x r') (EMetric.closedBall (f x) (ratio f * r')) := fun y hy =>
  (edist_eq f y x).trans_le <| mul_le_mul_left' hy _

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