closedBall_comp — Mathlib

English

With the same setup as Ball_comp, the closed ball behaves under composition as (p ∘ f).closedBall x r = f^{-1}( p.closedBall (f x) r ).

Русский

Та же установка, что и в Ball_comp, но для замкнутого шара: (p ∘ f).closedBall x r = f^{-1}( p.closedBall (f x) r ).

LaTeX

$$$((p \circ f).closedBall x r) = f^{-1}( p.closedBall (f x) r)$$$

Lean4

theorem closedBall_comp (p : Seminorm 𝕜₂ E₂) (f : E →ₛₗ[σ₁₂] E₂) (x : E) (r : ℝ) :
    (p.comp f).closedBall x r = f ⁻¹' p.closedBall (f x) r :=
  by
  ext
  simp_rw [closedBall, mem_preimage, comp_apply, Set.mem_setOf_eq, map_sub]

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