eventually_homothety_image_subset_of_finite_subset_interior

English

If t is finite and t ⊆ interior s, then eventually δ near 1 maps t by homothety into s.

Русский

Если t конечно и t ⊆ interior s, то существует окрестность 1 в ρ, такая что для всех δ в ней образ homothety(x,δ) тождественно отображается в s.

LaTeX

$$Finite(t) → t ⊆ interior(s) → ∀ᶠ δ in 𝓝(1), image((homothety x δ))(t) ⊆ s$$

Lean4

theorem _root_.eventually_homothety_image_subset_of_finite_subset_interior {t : Set Q} (ht : t.Finite)
    (h : t ⊆ interior s) : ∀ᶠ δ in 𝓝 (1 : R), homothety x δ '' t ⊆ s :=
  by
  suffices ∀ y ∈ t, ∀ᶠ δ in 𝓝 (1 : R), homothety x δ y ∈ s
    by
    simp_rw [Set.image_subset_iff]
    exact (Filter.eventually_all_finite ht).mpr this
  intro y hy
  exact eventually_homothety_mem_of_mem_interior R x (h hy)

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