preimage_iff — Mathlib

English

A set is ample iff its pre-image under a continuous affine equivalence is ample.

Русский

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

LaTeX

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

Lean4

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

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