English
Given suitable convex and boundary assumptions, there exists a gaugeRescaleEquiv e with the required image equalities for interior, closure, and frontier.
Русский
При подходящих условиях существ迷ет гомеоморфизм gaugeRescaleEquiv, обеспечивающий нужные изображения interior, closure и frontier.
LaTeX
$$$\\exists e : E \\simeq E,\\; e'' interior s = interior t \\;\\land\\; e'' closure s = closure t \\;\\land\\; e'' frontier s = frontier t$$$
Lean4
/-- Given two convex bounded sets in a topological vector space with nonempty interiors,
there exists a homeomorphism of the ambient space
that sends the interior, the closure, and the frontier of one set
to the interior, the closure, and the frontier of the other set.
In particular, if both `s` and `t` are open set or both `s` and `t` are closed sets,
then `e` maps `s` to `t`. -/
theorem exists_homeomorph_image_eq {s t : Set E} (hsc : Convex ℝ s) (hsne : (interior s).Nonempty)
(hsb : IsVonNBounded ℝ s) (hst : Convex ℝ t) (htne : (interior t).Nonempty) (htb : IsVonNBounded ℝ t) :
∃ e : E ≃ₜ E, e '' interior s = interior t ∧ e '' closure s = closure t ∧ e '' frontier s = frontier t :=
by
rsuffices ⟨e, h₁, h₂⟩ : ∃ e : E ≃ₜ E, e '' interior s = interior t ∧ e '' closure s = closure t
· refine ⟨e, h₁, h₂, ?_⟩
simp_rw [← closure_diff_interior, image_diff e.injective, h₁, h₂]
rcases hsne with ⟨x, hx⟩
rcases htne with ⟨y, hy⟩
set h : E ≃ₜ E := by
apply gaugeRescaleHomeomorph (-x +ᵥ s) (-y +ᵥ t) <;>
simp [← mem_interior_iff_mem_nhds, interior_vadd, mem_vadd_set_iff_neg_vadd_mem, *]
refine ⟨.trans (.addLeft (-x)) <| h.trans <| .addLeft y, ?_, ?_⟩
·
calc
(fun a ↦ y + h (-x + a)) '' interior s = y +ᵥ h '' interior (-x +ᵥ s) := by
simp_rw [interior_vadd, ← image_vadd, image_image, vadd_eq_add]
_ = _ := by rw [image_gaugeRescaleHomeomorph_interior, interior_vadd, vadd_neg_vadd]
·
calc
(fun a ↦ y + h (-x + a)) '' closure s = y +ᵥ h '' closure (-x +ᵥ s) := by
simp_rw [closure_vadd, ← image_vadd, image_image, vadd_eq_add]
_ = _ := by rw [image_gaugeRescaleHomeomorph_closure, closure_vadd, vadd_neg_vadd]
