preimage — Mathlib

English

Pre-images of ample sets under continuous affine equivalences are ample.

Русский

Прообраз ампельного множества под непрерывной аффинной эквивалентностью ампелен.

LaTeX

$$$\mathrm{AmpleSet}(s) \rightarrow \mathrm{AmpleSet}(L^{-1}'s)$$$

Lean4

/-- Pre-images of ample sets under continuous affine equivalences are ample. -/
theorem preimage {s : Set F} (h : AmpleSet s) (L : E ≃ᴬ[ℝ] F) : AmpleSet (L ⁻¹' s) :=
  by
  rw [← L.image_symm_eq_preimage]
  exact h.image L.symm

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