image_iff — Mathlib

English

An ample set is ample iff its image under a continuous affine equivalence is ample.

Русский

Ампельное множество сохраняется под изображением через непрерывную аффинную эквивалентность и обратно.

LaTeX

$$$\mathrm{AmpleSet}(L''s) \iff \mathrm{AmpleSet}(s)$$$

Lean4

/-- A set is ample iff its image under a continuous affine equivalence is. -/
theorem image_iff {s : Set E} (L : E ≃ᴬ[ℝ] F) : AmpleSet (L '' s) ↔ AmpleSet s :=
  ⟨fun h ↦ (L.symm_image_image s) ▸ h.image L.symm, fun h ↦ h.image L⟩

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